English
Let K and L be cochain complexes in a linear category C, and fix an integer a. For any integers n', n with n = n' + a, there is a canonical operation rightUnshift that takes a cochain γ: K → L⟦a⟧ of degree n' to a cochain of degree n: γ_rightUnshift ∈ Cochain(K, L) with components defined by composing γ against the shift isomorphism of L. This operation is functorial in the sense that it inverts a corresponding leftUnshift when degrees match, and it respects addition.
Русский
Пусть K и L – частично упорядоченные комплексы, в которых действует линейная категория C. Пусть a ∈ Z. Пусть n', n ∈ Z такие, что n = n' + a. Существуют канонические отображения rightUnshift: Cochain(K, L⟦a⟧)_{n'} → Cochain(K, L)_{n}, заданные на компонентах (p, q) формулой (γ.rightUnshift)_{p,q} = γ_{p,p+n'} ∘ shift Iso_L^a(p+n', q).hom. Эти отображения образуют морфизм комплексoв соседствующих степеней и образуют взаимно однічные пары с соответствующим leftUnshift; при сложении коCHAIN сохраняется аддитивность.
LaTeX
$$$\\text{rightUnshift}:\\;\\text{Cochain}(K,L\\langle a\\rangle)_{n'} \\to \\text{Cochain}(K,L)_{n},\\quad n' + a = n, \\\\ (\\text{rightUnshift}\\, \\gamma)_{p,q} = \\gamma_{p,p+n'} \\;\\circ\\; (L\\shiftFunctorObjXIso\\,a\\,(p+n',q)).hom$$$
Lean4
/-- The map `Cochain K (L⟦a⟧) n' → Cochain K L n` when `n' + a = n`. -/
def rightUnshift {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) : Cochain K L n :=
Cochain.mk
(fun p q hpq => γ.v p (p + n') rfl ≫ (L.shiftFunctorObjXIso a (p + n') q (by rw [← hpq, add_assoc, hn])).hom)
