English
Equality of the hom component for ShiftAdd' with the shift data, following from the defined equality.
Русский
Равенство гом-компоненты ShiftAdd' в соответствии с данными сдвига.
LaTeX
$$$$ \forall {C} [Category(C)], {a,b,ab}\in \mathbb{Z}, (h: a+b=ab) \Rightarrow ((\mathrm{shiftFunctorAdd'}(CochainComplex,ℤ) a b ab h).hom.app K).f n = (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom. $$$$
Lean4
instance commShiftMapCochainComplex : (F.mapHomologicalComplex (ComplexShape.up ℤ)).CommShift ℤ
where
iso := F.mapCochainComplexShiftIso
zero := by
ext
rw [CommShift.isoZero_hom_app]
dsimp
simp only [CochainComplex.shiftFunctorZero_inv_app_f, CochainComplex.shiftFunctorZero_hom_app_f,
HomologicalComplex.XIsoOfEq, eqToIso, eqToHom_map, eqToHom_trans, eqToHom_refl]
add := fun a b => by
ext
rw [CommShift.isoAdd_hom_app]
dsimp
rw [id_comp, id_comp]
simp only [CochainComplex.shiftFunctorAdd_hom_app_f, CochainComplex.shiftFunctorAdd_inv_app_f,
HomologicalComplex.XIsoOfEq, eqToIso, eqToHom_map, eqToHom_trans, eqToHom_refl]
