English
For any morphism f: X → Y and Z, Mono, cokernel.π f = 0, and (f,0) form an exact short complex, all are equivalent to Epi f.
Русский
Для морфизма f: X → Y и Z утверждения Mono f, cokernel.π f = 0 и точность краткой последовательности (f,0) эквивалентны эпиморфизму f.
LaTeX
$$TFAE [Epi f, cokernel.π f = 0, (ShortComplex.mk f (0 : Y ⟶ Z) comp_zero).Exact]$$
Lean4
theorem tfae_epi {X Y : C} (f : X ⟶ Y) (Z : C) :
TFAE [Epi f, cokernel.π f = 0, (ShortComplex.mk f (0 : Y ⟶ Z) comp_zero).Exact] :=
by
tfae_have 2 → 1 := epi_of_cokernel_π_eq_zero _
tfae_have 1 → 2
| _ => by rw [← cancel_epi f, cokernel.condition, comp_zero]
tfae_have 3 ↔ 1 := ShortComplex.exact_iff_epi _ (by simp)
tfae_finish