isZero_cokernel_of_epi — Mathlib

English

If f is an epimorphism and has a cokernel, then the cokernel is the zero object.

Русский

Если f является эпиморфизмом и существует котокernel, то его котокernel является нулевым объектом.

LaTeX

$$$\forall {C} [Category C] [HasZeroMorphisms C] {X Y} (f : X ⟶ Y) [Epi f] [HasCokernel f], IsZero (cokernel f)$$$

Lean4

theorem isZero_cokernel_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] [HasCokernel f] : IsZero (cokernel f) :=
  CokernelCofork.IsColimit.isZero_of_epi (c := CokernelCofork.ofπ _ (cokernel.condition f)) (cokernelIsCokernel f)

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