English
The leftShift of a cochain γ under a is connected to the δ of γ by a neg-one-power factor: δ n' m' (γ.leftShift a n' hn') = a.negOnePow · (δ n m γ).leftShift a m' hm'.
Русский
Левый сдвиг γ связан с δ через фактор (-1)^a: δ n' m' (γ.leftShift a n' hn') = a.negOnePow · (δ n m γ).leftShift a m' hm'.
LaTeX
$$$\delta n' m' (\gamma.leftShift a n' hn') = a.negOnePow · (\delta n m γ).leftShift a m' hm'$$$
Lean4
theorem δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) :
δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm' :=
by
by_cases hnm : n + 1 = m
· have hnm' : n' + 1 = m' := by omega
ext p q hpq
dsimp
rw [(δ n m γ).rightShift_v a m' hm' p q hpq _ rfl, δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by cutsat) rfl,
δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by cutsat) rfl, γ.rightShift_v a n' hn' p (p + n') rfl (p + n) rfl,
γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by cutsat)]
simp only [shiftFunctorObjXIso, shiftFunctor_obj_d', Linear.comp_units_smul, assoc,
HomologicalComplex.XIsoOfEq_inv_comp_d, add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp,
smul_add, add_right_inj, smul_smul]
simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
· have hnm' : ¬n' + 1 = m' := fun _ => hnm (by cutsat)
rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]
