English
Compatibility of the D1-differential with the total shift in the second index: the shifted D1 is related to the original by D1-shift iso, up to the appropriate sign.
Русский
Совместимость D1-дифференциала с общим сдвигом по второму индексу: сдвинутый D1 связан с исходным через D1-shift izo с учётом знака.
LaTeX
$$$D₁_{totalShift₂XIso-hom}$$$
Lean4
@[reassoc]
theorem D₁_totalShift₂XIso_hom (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') :
((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
y.negOnePow • ((K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁') :=
by
by_cases h : (up ℤ).Rel n₀ n₁
· apply total.hom_ext
intro p q hpq
dsimp at h hpq
dsimp [totalShift₂XIso]
rw [ι_D₁_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₁, smul_smul,
((shiftFunctor₂ C y).obj K).d₁_eq _ rfl _ _ (by dsimp; cutsat), K.d₁_eq _ rfl _ _ (by dsimp; cutsat)]
dsimp
rw [one_smul, one_smul, Category.assoc, ι_totalDesc, Linear.comp_units_smul, ← Int.negOnePow_add]
congr 2
linarith
· rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]
grind [up_Rel]
