English
The v-component of the shifted cochain (γ.shift a) is given by the explicit formula: (γ.shift a).v p q hpq equals the composition of the shifted K-iso on p and the shifted L-iso on q with γ.v at the shifted indices p', q'.
Русский
Компонента v сдвинутого коцепного γ.shift a задаётся явной формулой: (γ.shift a).v p q hpq равна композиции изоморфизмов сдвига K на p и L на q с γ.v в смещённых индексах p', q'.
LaTeX
$$$\\big(\\gamma.shift a\\big).v_{p q}^{hpq} = (K.shiftIso\\,a\\;p, p') \\circ γ_{v}^{p' q'} \\circ (L.shiftIso\\,a\\; q, q')^{-1}$$$
Lean4
theorem shift_v (a : ℤ) (p q : ℤ) (hpq : p + n = q) (p' q' : ℤ) (hp' : p' = p + a) (hq' : q' = q + a) :
(γ.shift a).v p q hpq =
(K.shiftFunctorObjXIso a p p' hp').hom ≫
γ.v p' q' (by rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]) ≫
(L.shiftFunctorObjXIso a q q' hq').inv :=
by
subst hp' hq'
rfl
