rightShift — Mathlib

English

The composition of the left shift and the right shift on a cochain is equal to the shift by a, up to the same sign factor as above, showing a symmetric sign phenomenon for shifts.

Русский

Состав левого сдвига и правого сдвига на коцепне равен сдвигу на a с тем же знаком, что и в предыдущих формулах, демонстрируя симметричное поведение знака при сдвигах.

LaTeX

$$$ (\gamma^{\mathrm{leftShift}}(a,n',hn'))^{\mathrm{rightShift}}(a,n,hn') = (-1)^{a\,n' + \frac{a(a-1)}{2}} \; γ^{\mathrm{shift}}(a). $$$

Lean4

/-- The map `Cocycle K L n → Cocycle K (L⟦a⟧) n'` when `n' + a = n`. -/
@[simps!]
def rightShift (γ : Cocycle K L n) (a n' : ℤ) (hn' : n' + a = n) : Cocycle K (L⟦a⟧) n' :=
  Cocycle.mk (γ.1.rightShift a n' hn') _ rfl
    (by
      simp only [Cochain.δ_rightShift _ a n' (n' + 1) hn' (n + 1) (by cutsat), δ_eq_zero, Cochain.rightShift_zero,
        smul_zero])

Похожие утверждения