English
Compatibility of the D1-differential with the total shift in the first index, including the sign behavior: the shifted D1 equals the original D1 composed with the shift isomorphism up to the sign given by the shift.
Русский
Совместимость D1-дифференциала с общим сдвигом по первому индексу с учётом знака: сдвиг D1 равен D1 после композиции с изоморфизмом сдвига, до знака.
LaTeX
$$$D₁_{totalShift1XIso-hom}$ expresses$\\; D₁$-compatibility with totalShift1XIso hom component (including sign).$$
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 _ (show p + x + 1 = p + 1 + x by cutsat) _ _ (by dsimp; cutsat)]
dsimp
rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]
· rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]
grind [up_Rel]
