English
There is a shift operator on Cochain complexes: for a given a ∈ Z, a morphism γ ∈ Cochain(K⟦a⟧, L⟦a⟧) n, yields a corresponding morphism γ.shift a ∈ Cochain(K⟦a⟧, L⟦a⟧) n with a reindexed domain and codomain via canonical shift isomorphisms.
Русский
Существует оператор сдвига на коцепных комплексах: для данного a ∈ Z морфизм γ ∈ Cochain(K⟦a⟧, L⟦a⟧) n получает соответствующий морфизм γ.shift a ∈ Cochain(K⟦a⟧, L⟦a⟧) n с перераспределением индексов через канонические изоморфии сдвига.
LaTeX
$$$\\text{shift}(a):\\;\\text{Cochain}(K\\langle a\\rangle, L\\langle a\\rangle)_{n} \\to \\text{Cochain}(K\\langle a\\rangle, L\\langle a\\rangle)_{n}, \\quad (\\gamma\\shift a)_{p,q} = (K\\shiftIso)_{a,p,p'} \\circ γ_{p',q'} \\circ (L\\shiftIso)_{a,q,q'}^{-1}$$$
Lean4
/-- The map `Cochain K L n → Cochain (K⟦a⟧) (L⟦a⟧) n`. -/
def shift (a : ℤ) : Cochain (K⟦a⟧) (L⟦a⟧) n :=
Cochain.mk
(fun p q hpq =>
(K.shiftFunctorObjXIso a p _ rfl).hom ≫ γ.v (p + a) (q + a) (by cutsat) ≫ (L.shiftFunctorObjXIso a q _ rfl).inv)
