exact_iff_iCycles_pOpcycles_zero — Mathlib

English

Let S be a Short Complex with homology. Then S is exact if and only if the composite S.iCycles ≫ S.pOpcycles vanishes.

Русский

Пусть S — краткий комплекс с гомологией. Тогда S точен тогда, когда композиция S.iCycles ≫ S.pOpcycles равна нулю.

LaTeX

$$$ \\mathrm{Exact}(S) \\iff S.iCycles \\circ S.pOpcycles = 0 $$$

Lean4

theorem exact_iff_iCycles_pOpcycles_zero [S.HasHomology] : S.Exact ↔ S.iCycles ≫ S.pOpcycles = 0 :=
  S.exact_iff_i_p_zero _ _

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