exact_iff_exact_coimage_π — Mathlib

English

Exactness of S is equivalent to the exactness of the coimage map π with respect to g.

Русский

Точность S эквивалентна точности отображения кообразования π по отношению к g.

LaTeX

$$$S.Exact \\iff (ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero)).Exact$$$

Lean4

theorem exact_iff_exact_coimage_π :
    S.Exact ↔ (ShortComplex.mk S.f (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero)).Exact :=
  by
  symm
  exact
    ShortComplex.exact_iff_of_epi_of_isIso_of_mono
      { τ₁ := 𝟙 _
        τ₂ := 𝟙 _
        τ₃ := Abelian.factorThruCoimage S.g }

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