English
The homology functor on the up-shifted complex carries a ShiftSequence structure by integers, giving a natural way to compare shifts and homology across degrees.
Русский
Гомологическая функция на смещенном вверх комплексe обладает структурой ShiftSequence по целым числам, задавая естественный способ сравнивать сдвиги и гомологию по степеням.
LaTeX
$$$ (\\mathrm{homologyFunctor} (C, \\mathrm{up} \\mathbb{Z}) 0).\\mathrm{ShiftSequence} \\mathbb{Z} $$$
Lean4
noncomputable instance : (homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ
where
sequence n := homologyFunctor C (ComplexShape.up ℤ) n
isoZero := Iso.refl _
shiftIso n a a' ha' := ShiftSequence.shiftIso C n a a' ha'
shiftIso_zero
a := by
ext K
dsimp [homologyMap]
simp only [ShiftSequence.shiftIso_hom_app, comp_id, shiftShortComplexFunctorIso_zero_add_hom_app]
shiftIso_add n m a a' a'' ha'
ha'' := by
ext K
dsimp [homologyMap]
simp only [ShiftSequence.shiftIso_hom_app, id_comp, ← ShortComplex.homologyMap_comp,
shiftFunctorAdd'_eq_shiftFunctorAdd, shiftShortComplexFunctorIso_add'_hom_app n m _ rfl a a' a'' ha' ha'' K]
