English
Compatibility of the D2-differential with the total shift in the first index: the shifted D2 is related to the original D2 via the totalShift1XIso-hom up to the sign given by the shift.
Русский
Совместимость D2-дифференциала с общим сдвигом по первому индексу: сдвиг D2 связан с исходным D2 через totalShift1XIso-hom с учётом знака сдвига.
LaTeX
$$$D₂_{totalShift1XIso-hom}$ expresses relation between D₂ and totalShift1XIso-hom.$$
Lean4
@[reassoc]
theorem D₂_totalShift₁XIso_hom (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') :
((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
x.negOnePow • ((K.totalShift₁XIso x 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, ι_D₂,
((shiftFunctor₁ C x).obj K).d₂_eq _ _ rfl _ (by dsimp; cutsat), K.d₂_eq _ _ rfl _ (by dsimp; cutsat), smul_smul,
Linear.units_smul_comp, Category.assoc, ι_totalDesc]
dsimp
congr 1
rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
· rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
grind [up_Rel]
