epi_as_hom''_mkQ

Mathlib.Algebra.Category.ModuleCat.EpiMono

URI: https://scilib.ai/kg/mathlib#ModuleCat.epi_as_hom''_mkQ

English

The quotient map X → X/U is an epimorphism in ModuleCat.

Русский

Кватирование X → X/U является эпиморфизмом в ModuleCat.

LaTeX

$$$\\text{ModuleCat.ofHom}(U.mkQ)$ is epi.$$

Lean4

instance epi_as_hom''_mkQ (U : Submodule R X) : Epi (ModuleCat.ofHom U.mkQ) :=
  (epi_iff_range_eq_top _).mpr <| Submodule.range_mkQ _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru