English
For γ ∈ Cochain(K⟦a⟧) L n' and suitable data, the v-component of (γ.leftUnshift n hn) is explicitly given by the combination of the shift iso on K and the original v-component γ.v with index shifts.
Русский
Для γ ∈ Cochain(K⟦a⟧) L n' и подходящих данных, векторная компонента v у (γ.leftUnshift n hn) задаётся через сдвиговые изоморфизмы K и исходную компоненту v γ.
LaTeX
$$$\\big(\\gamma.leftUnshift\\,n\\,hn\\big)_{v}\\;=\; (a n' + \\frac{a(a-1)}{2})\\!\\text{NegOnePow} \\cdot (K\\shiftFunctorObjXIso a (p') p)_{}^{-1} \\;\\circ\\; \\gamma_{v}(p',q),$$$
Lean4
theorem leftUnshift_v {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') (p q : ℤ) (hpq : p + n = q)
(p' : ℤ) (hp' : p' + n' = q) :
(γ.leftUnshift n hn).v p q hpq =
(a * n' + ((a * (a - 1)) / 2)).negOnePow •
(K.shiftFunctorObjXIso a p' p (by cutsat)).inv ≫ γ.v p' q (by cutsat) :=
by
obtain rfl : p' = p - a := by cutsat
rfl
