English
There is a leftUnshift operation that, given γ ∈ Cochain(K⟦a⟧) L n' and integers n,a with n + a = n', produces a cochain in Cochain(K,L) with degree n. The construction uses a scalar factor depending on a and n', together with the shift isomorphism on K.
Русский
Существует операция leftUnshift, для данного γ ∈ Cochain(K⟦a⟧) L n' и целых n,a с условием n + a = n', которая дает коцепную стрелку в Cochain(K,L) с степенью n. Конструкция включает скалярный множитель, зависящий от a и n', и сдвиговую изоморфию на K.
LaTeX
$$$\\text{leftUnshift}:\\;\\text{Cochain}(K\\langle a\\rangle, L)_{n'} \\to \\text{Cochain}(K,L)_{n},\\quad n + a = n', \\\\ (\\text{leftUnshift}\\;\\gamma)_{p,q} = \\left( a n' + \\frac{a(a-1)}{2} \\right)\\!\\text{NegOnePow} \\cdot (K\\shiftFunctorObjXIso a (p-a),p)^{-1} \\circ \\gamma_{p-a,q},$$
Lean4
/-- The map `Cochain (K⟦a⟧) L n' → Cochain K L n` when `n + a = n'`. -/
def leftUnshift {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : Cochain K L n :=
Cochain.mk
(fun p q hpq =>
(a * n' + ((a * (a - 1)) / 2)).negOnePow •
(K.shiftFunctorObjXIso a (p - a) p (by cutsat)).inv ≫ γ.v (p - a) q (by cutsat))
