English
For even j with prev j → j and j → next j, the j-th homology of alternatingConst is isomorphic to the homology of ShortComplex.mk ψ φ hEven.
Русский
Для чётного j, когда prev(j) ≈ j и j ≈ next(j), j-я гомология alternatingConst изоморфна гомологии ShortComplex.mk ψ φ hEven.
LaTeX
$$$\text{AltConstHomologyIsoEven}(A, hOdd, hEven, hc).homology\, j \cong \mathrm{ShortComplex.mk}\; ψ\; φ\; hEven$.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 even. -/
noncomputable def alternatingConstHomologyIsoEven [CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j)
(hnj : c.Rel j (c.next j)) (h : Even j) :
(alternatingConst A hOdd hEven hc).homology j ≅ (ShortComplex.mk ψ φ hEven).homology :=
ShortComplex.homologyMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)
