English
A variant of the odd-case homology iso asserting equivalence of maps under canonical refls for the Odd case.
Русский
Вариант нечётного случая изоморфизма гомологии, утверждающий эквивалентность отображений под каноническими тождествами.
LaTeX
$$$\text{AltConstHomologyIsoOdd}(A, hOdd, hEven, hc).homology\, j \cong \mathrm{ShortComplex.mk}\; φ\; ψ\; hOdd$.homology$$
Lean4
/-- The chain complex `X ←0- X ←𝟙- X ←0- X ←𝟙- X ⋯`.
It is exact away from `0` and has homology `X` at `0`. -/
@[simps]
noncomputable def alternatingConst [HasZeroMorphisms C] : C ⥤ ChainComplex C ℕ
where
obj
X :=
HomologicalComplex.alternatingConst X (Category.id_comp 0) (Category.comp_id 0)
(fun _ _ => ComplexShape.down_nat_odd_add)
map {X Y}
f :=
{ f _ := f
comm' i j hij := by by_cases Even i <;> simp_all [-Nat.not_even_iff_odd] }
