alternatingConstHomologyDataOdd — Mathlib

English

Further odd-case iso between the homology of alternatingConst and the homology of the corresponding short complex.

Русский

Дополнительный нечётный случай изоморфизма гомологии alternatingConst и гомологии соответствующего короткого комплекса.

LaTeX

$$$\text{AltConstHomologyIsoOdd}(A, hOdd, hEven, hc).homology\, j \cong \mathrm{ShortComplex.mk}\; φ\; ψ\; hOdd$.homology$$

Lean4

/-- The `n`-th homology of the alternating constant complex is zero for odd `n`. -/
noncomputable def alternatingConstHomologyDataOdd (X : C) (n : ℕ) (hn : Odd n) :
    ((alternatingConst.obj X).sc n).HomologyData :=
  .ofIsColimitCokernelCofork _ (by simp [hn]) _ (Limits.zeroCokernelOfZeroCancel _ (by simp [hn]))

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