epi_iff_surjective — Mathlib

English

Epi f is equivalent to Surjective ((forget₂ C Ab).map f).

Русский

Эпиморфизм f эквивалентен сюръективности отображения forget₂ C Ab.

LaTeX

$$$$ \\operatorname{Epi}(f) \\iff \\operatorname{Surjective}\\left( (\\mathrm{forget}_{2} C Ab).map f \\right). $$$$

Lean4

theorem epi_iff_surjective {X Y : C} (f : X ⟶ Y) : Epi f ↔ Function.Surjective ((forget₂ C Ab).map f) :=
  by
  rw [← AddCommGrpCat.epi_iff_surjective]
  constructor
  · intro
    infer_instance
  · apply Functor.epi_of_epi_map

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