alternatingConstHomologyZero — Mathlib

English

Even-case iCycles map is zero when composed with φ.

Русский

Чётный случай: iCycles-компонента композиция с φ равна нулю.

LaTeX

$$$((\mathrm{alternatingConst}\; A\; hOdd\; hEven\; hc).iCycles\, j)\;\circ φ = 0$$$

Lean4

/-- The `n`-th homology of the alternating constant complex is `X` for `n = 0`. -/
noncomputable def alternatingConstHomologyZero (X : C) : (alternatingConst.obj X).homology 0 ≅ X :=
  (alternatingConstHomologyDataZero X _ rfl).left.homologyIso

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