English
For a fixed γ in Cochain(K, L n) and appropriate integers n, n', a and p, p', the v-component of the rightUnshift of γ is given by composing the original v-component with the shift isomorphism on L. This describes how the vertical component behaves under rightUnshift.
Русский
Для фиксированного γ ∈ Cochain(K, L) и допустимых целых чисел n, n', a, p, p' описывается выражение компоненты v после применения rightUnshift: (γ.rightUnshift n hn).v_{p q} = γ_{p p'} ∘ shiftIso^L_{a}(p', q).hom.
LaTeX
$$$\\text{For suitable } p,q,p',\\; (\\gamma.\\text{rightUnshift}\\,n\\,hn)_{v}(p,q) = \\gamma_{v}(p,p') \\;\\circ\\; (L\\shiftFunctorObjXIso\\,a\\,p'\\,q)(\\text{hom})$$$
Lean4
theorem rightUnshift_v {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) (p q : ℤ) (hpq : p + n = q)
(p' : ℤ) (hp' : p + n' = p') :
(γ.rightUnshift n hn).v p q hpq =
γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a p' q (by rw [← hpq, ← hn, ← add_assoc, hp'])).hom :=
by
subst hp'
dsimp only [rightUnshift]
simp only [mk_v]
