exact_iff_i_p_zero — Mathlib

English

Let S be a Short Complex in a category with zero morphisms. Then S is exact if and only if the composite h1.i ≫ h2.p vanishes, where h1 and h2 are the Left and Right Homology data for S.

Русский

Пусть S — краткий комплекс в категории с нулевыми морфизмами. Тогда S точен тогда, когда композиция h1.i ≫ h2.p равна нулю, где h1 и h2 — данные левой и правой гомологии S.

LaTeX

$$$ \\mathrm{Exact}(S) \\iff h_1.i \\circ h_2.p = 0 $$$

Lean4

theorem exact_iff_i_p_zero [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
    S.Exact ↔ h₁.i ≫ h₂.p = 0 :=
  (HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).exact_iff_i_p_zero

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