English
The left shift interacts with composition: leftShift of γ . γ' equals a scaled left shift of γ composed with γ', with a sign depending on a.
Русский
Левый сдвиг взаимодействует с композицией: левый сдвиг γ . γ' эквивалентен композиции левого сдвига γ с γ' с множителем и знаком.
LaTeX
$$$ (\gamma .\gamma')^{leftShift} = a.negOnePow · (\gamma.leftShift a n' hn').comp γ' $$$
Lean4
theorem leftShift_comp (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : Cochain L M m) (h : n + m = t)
(ht' : t + a = t') :
(γ.comp γ' h).leftShift a t' ht' =
(a * m).negOnePow •
(γ.leftShift a n' hn').comp γ' (by rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]) :=
by
ext p q hpq
have h' : n' + m = t' := by omega
dsimp
simp only [Cochain.comp_v _ _ h' p (p + n') q rfl (by cutsat),
γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by cutsat),
(γ.comp γ' h).leftShift_v a t' (by cutsat) p q hpq (p + a) (by cutsat), smul_smul, Linear.units_smul_comp, assoc,
Int.negOnePow_add, ← mul_assoc, ← h', comp_v _ _ h (p + a) (p + n') q (by cutsat) (by cutsat)]
congr 2
rw [add_comm n', mul_add, Int.negOnePow_add]
