English
Analogous to totalShift1Iso_hom_f, but for shifts in the second index: the iotaTotal (total) component interacts with the totalShift₂Iso_hom_f in a sign-sensitive way.
Русский
Аналогично для сдвига по второму индексу: компонент iotaTotal взаимодействует с totalShift₂Iso_hom_f с учётом знака.
LaTeX
$$$ι\\_totalShift₂Iso\\_hom\\_f$ expresses the relation between total shifts in the second index and iotaTotal.$$
Lean4
/-- Auxiliary definition for `totalShift₂Iso`. -/
noncomputable def totalShift₂XIso (n n' : ℤ) (h : n + y = n') :
(((shiftFunctor₂ C y).obj K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X n'
where
hom := totalDesc _ (fun p q hpq => (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' (by dsimp at hpq ⊢; omega))
inv :=
totalDesc _
(fun p q hpq =>
(p * y).negOnePow •
(K.XXIsoOfEq _ _ _ rfl (Int.sub_add_cancel q y)).inv ≫
((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n (by dsimp at hpq ⊢; omega))
hom_inv_id := by
ext p q h
dsimp
simp only [ι_totalDesc_assoc, Linear.units_smul_comp, ι_totalDesc, smul_smul, Int.units_mul_self, one_smul, comp_id]
exact ((shiftFunctor₂ C y).obj K).XXIsoOfEq_inv_ιTotal _ rfl (by omega) _ _
inv_hom_id := by
ext
dsimp
simp only [ι_totalDesc_assoc, Linear.units_smul_comp, Category.assoc, ι_totalDesc, Linear.comp_units_smul,
XXIsoOfEq_inv_ιTotal, smul_smul, Int.units_mul_self, one_smul, comp_id]
