English
Let C be a category with additive structure. For cochain complexes over C indexed by the integers, the shift functors satisfy the usual additivity compatibility: for integers n1, n2, n12 with n1 + n2 = n12, there is a canonical natural isomorphism shift(C, n12) ≅ shift(C, n1) ∘ shift(C, n2).
Русский
Пусть C — категория с аддитивной структурой. Для кограционной композиции над C индексации по целым числам существует каноническое натуральное изоморфизм: сдвиг на n12 эквивалентен композиции сдвигов на n1 и n2, если n1 + n2 = n12.
LaTeX
$$$$\forall C\,[C:\\text{Category}]\,\forall n_1,n_2,n_{12}\in \mathbb{Z},\ n_1+n_2=n_{12} \Rightarrow \exists \alpha:\ \mathrm{Shift}(C,n_{12}) \cong \ \mathrm{Shift}(C,n_1) \circ \mathrm{Shift}(C,n_2).$$$$
Lean4
/-- The compatibility of the shift functors on `CochainComplex C ℤ` with respect
to the addition of integers. -/
@[simps!]
def shiftFunctorAdd' (n₁ n₂ n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂) : shiftFunctor C n₁₂ ≅ shiftFunctor C n₁ ⋙ shiftFunctor C n₂ :=
NatIso.ofComponents
(fun K =>
Hom.isoOfComponents (fun i => K.shiftFunctorObjXIso _ _ _ (by cutsat))
(fun _ _ _ => by
subst h
dsimp
simp only [add_comm n₁ n₂, Int.negOnePow_add, Linear.units_smul_comp, Linear.comp_units_smul,
d_comp_XIsoOfEq_hom, smul_smul, XIsoOfEq_hom_comp_d]))
(by intros; ext; simp)
