English
The D2-differential remains compatible with the total shift in the second index; the shifted iso interacts with D2 similarly to D1.
Русский
Совместимость D2 с общим сдвигом по второму индексу; сдвинутый изоморфизм взаимодействует с D2 аналогично D1.
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, smul_smul, ι_D₂,
((shiftFunctor₂ C y).obj K).d₂_eq _ _ rfl _ (by dsimp; cutsat),
K.d₂_eq _ _ (show q + y + 1 = q + 1 + y by cutsat) _ (by dsimp; cutsat), Linear.units_smul_comp, Category.assoc,
smul_smul, ι_totalDesc]
dsimp
rw [Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, smul_smul, ← Int.negOnePow_add, ← Int.negOnePow_add,
← Int.negOnePow_add, ← Int.negOnePow_add]
congr 2
cutsat
· rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
simp_all only [up_Rel]
grind
