English
Two-parameter δ identities linking leftShift and leftUnshift, showing the combinatorial compatibility of δ with both shifts with arithmetic relations on the indices.
Русский
Два варианта идентичности δ, связывающих leftShift и leftUnshift, показывающих совместимость δ с обоими сдвигами и арифметическими отношениями индексов.
LaTeX
$$$\delta_{n,m}(\gamma.leftShift a n' hn) = a.negOnePow · (\delta n' m' γ).leftUnshift m hm'$$$
Lean4
@[simp]
theorem δ_shift (a m : ℤ) : δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a :=
by
by_cases hnm : n + 1 = m
· ext p q hpq
dsimp
simp only [shift_v', shiftFunctor_obj_d', δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
δ_v n m hnm _ (p + a) (q + a) (by cutsat) (q - 1 + a) (p + 1 + a) (by cutsat) (by cutsat), smul_add,
Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj]
rw [smul_comm]
· rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_zero, smul_zero]
