tfae_epi — Mathlib

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

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