exactAt_iff_isZero_homology — Mathlib

English

Let K be a homological complex. Then at index i, K is exact iff the i-th homology vanishes.

Русский

Пусть K — гомологический комплекс. Тогда точность на индексе i эквивалентна нулевой i-й гомологии.

LaTeX

$$$ \operatorname{ExactAt}_i(K) \Longleftrightarrow H_i(K) = 0 $$$

Lean4

theorem exactAt_iff_isZero_homology [K.HasHomology i] : K.ExactAt i ↔ IsZero (K.homology i) :=
  by
  dsimp [homology]
  rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]

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