leftShift_v — Mathlib

English

The v-component of the right shift of a cocycle γ by a is given by a linear combination of a and a-1 terms times the isomorphism coming from the shift functor.

Русский

v-компонент правого сдвига кокейн-ядра γ на a задаётся линейной комбинацией коэффициентов, умноженной на изоморфизм из сдвиг-префунктора.

LaTeX

$$$\\text{rightShift\_v}(\\gamma, a, n') = (a n' + \\frac{a(a-1)}{2})\\cdot \\text{negOnePow} \\; \\gamma_{\\text{v}}(p,p',p') \\text{ etc.}$$$

Lean4

theorem leftShift_v (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q) :
    (γ.leftShift a n' hn').v p q hpq =
      (a * n' + ((a * (a - 1)) / 2)).negOnePow •
        (K.shiftFunctorObjXIso a p p' (by rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq])).hom ≫
          γ.v p' q hp' :=
  by
  obtain rfl : p' = p + a := by cutsat
  dsimp only [leftShift]
  simp only [mk_v]

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