exact_iff_homology_iso_zero — Mathlib

English

A ShortComplex S is exact if and only if there exists an isomorphism between its homology and the zero object.

Русский

Краткий комплекс S точен тогда, когда существует изоморфизм гомологии S с нулевым объектом.

LaTeX

$$$S.Exact \\iff (\\exists \\; h:\\; S.homology \\cong 0)$$$

Lean4

theorem exact_iff_homology_iso_zero [S.HasHomology] [HasZeroObject C] : S.Exact ↔ Nonempty (S.homology ≅ 0) :=
  by
  rw [exact_iff_isZero_homology]
  constructor
  · intro h
    exact ⟨h.isoZero⟩
  · rintro ⟨e⟩
    exact IsZero.of_iso (isZero_zero C) e

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