English
There are compatibility identities linking δ with both leftShift and leftUnshift, expressing that δ commutes with those shift operations up to sign twists depending on a.
Русский
Существуют совместимые соотношения δ с левым сдвигом и левым Unshift, выражающие, что δ коммутирует с этими операциями сдвига с учётом знаковых множителей.
LaTeX
$$$\text{δ_leftUnshift} \;\text{и}\; \text{δ_leftShift}$$$
Lean4
theorem δ_leftShift (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m') :
δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift 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 γ).leftShift_v a m' hm' p q hpq (p + a) (by cutsat),
δ_v n m hnm _ (p + a) q (by cutsat) (p + n') (p + 1 + a) (by cutsat) (by cutsat),
δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by cutsat) rfl,
γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by cutsat),
γ.leftShift_v a n' hn' (p + 1) q (by cutsat) (p + 1 + a) (by cutsat)]
simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp,
Linear.units_smul_comp, shiftFunctor_obj_d', Linear.comp_units_smul, smul_add, smul_smul]
congr 2
· rw [← hnm', add_comm n', mul_add, mul_one]
simp only [Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
· simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]
congr 1
linarith
· have hnm' : ¬n' + 1 = m' := fun _ => hnm (by cutsat)
rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_zero, smul_zero]
