epi_iff_range_eq_top — Mathlib

English

For morphism f: A ⟶ B in CommGrpCat, f is epi if and only if the underlying homomorphism f.hom has range equal to the top subgroup of B.

Русский

Для морфизма f: A → B в CommGrpCat, f является эпиморфизмом тогда и только тогда, когда образ f.hom равен верхней подгруппе B.

LaTeX

$$$$ \mathrm{Epi}(f) \iff f.\mathrm{hom.range} = \top $$$$

Lean4

@[to_additive]
theorem epi_iff_range_eq_top : Epi f ↔ f.hom.range = ⊤ :=
  ⟨fun _ => range_eq_top_of_epi _, fun hf =>
    ConcreteCategory.epi_of_surjective _ <| show Function.Surjective f.hom from MonoidHom.range_eq_top.mp hf⟩

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