range_eq_top_of_epi — Mathlib

English

If f is an epimorphism in CommGrpCat, then the range of the underlying group homomorphism f.hom equals the top subgroup of B; equivalently f is surjective.

Русский

Если f является эпиморфизмом в CommGrpCat, то образ f.hom равен верхней подгруппе B; то есть отображение сюръективно.

LaTeX

$$$$ [\mathrm{Epi}(f)] \Rightarrow f.\mathrm{hom.range} = \top $$$$

Lean4

@[to_additive]
theorem range_eq_top_of_epi [Epi f] : f.hom.range = ⊤ :=
  MonoidHom.range_eq_top_of_cancel fun u v h =>
    ConcreteCategory.ext_iff.mp <| (@cancel_epi _ _ _ _ _ f _ (ofHom u) (ofHom v)).1 (ConcreteCategory.ext h)

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