CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift

theorem CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n''), (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

This theorem states that for any category `C` with preadditive structure, given any two cochain complexes `K` and `L` in `C`, a cochain `γ` of any degree `n` between `K` and `L`, and integers `a`, `n'`, `n''` such that `n' + a = n` and `n + a = n''`, the left shift followed by the right shift of the cochain `γ` is equal to the right shift followed by the left shift of `γ`, up to a factor of `(-1)^a`. The left and right shifts here are operations performed on the complexes or cochains, akin to shifting their indices. The factor `(-1)^a` expresses the "sign" that the theorem mentions.

More concisely: For any cochain complexes K and L in a preadditive category C, and any cochain γ of degree n, the commutativity of left and right shifts of γ holds up to a sign: (L[n'] → K[n''] ≈ K[n'] → L[n'']), where n' + a = n and n + a = n'', with shift operators and a being integers.