English
For odd j, prev j ~ j and j ~ next j, the j-th homology of alternatingConst is isomorphic to the homology of ShortComplex.mk φ ψ hOdd.
Русский
Для нечётного j, когда prev(j) ~ j и j ~ next(j), j-я гомология alternatingConst изоморфна гомологии ShortComplex.mk φ ψ hOdd.
LaTeX
$$$\text{AltConstHomologyIsoOdd}(A, hOdd, hEven, hc).homology\, j \cong \mathrm{ShortComplex.mk}\; φ\; ψ\; hOdd$.homology$$
Lean4
/-- The `j`th homology of the alternating constant complex on `φ, ψ : A ⟶ A` is the homology of
`A --φ--> A --ψ--> A` when `prev(j) ~ j, j ~ next(j)` and `j` is odd. -/
noncomputable def alternatingConstHomologyIsoOdd [CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j)
(hnj : c.Rel j (c.next j)) (h : Odd j) :
(alternatingConst A hOdd hEven hc).homology j ≅ (ShortComplex.mk φ ψ hOdd).homology :=
ShortComplex.homologyMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)
