epi_iff_isZero_cokernel' — Mathlib

English

Equivalence: f is epi iff cokernel f is zero (via cokernel cofork' argument).

Русский

Эквивалентность: f эпиморфизм тогда и только тогда, когда cokernel f = 0.

LaTeX

$$$\operatorname{Epi}(f) \iff \operatorname{IsZero}(\operatorname{cokernel}(f))$$$

Lean4

theorem epi_iff_isZero_cokernel' {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c) :
    Epi f ↔ IsZero c.pt :=
  ⟨fun _ ↦ CokernelCofork.IsColimit.isZero_of_epi hc, epi_of_isZero_cokernel' c hc⟩

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