leftUnshift — Mathlib

English

There is a leftUnshift operation: given a cocycle on K⟦a⟧ and a degree n with n' + a = n, one obtains a cocycle on K with degree n. This is the reverse operation to rightUnshift.

Русский

Существет операция leftUnshift: кокцикл на K⟦a⟧ и n' с условием n' + a = n даёт кокцикл на K и n, обратная к rightUnshift.

LaTeX

$$$\mathrm{leftUnshift}: \text{Cocycle}(K⟦a⟧,(L),n') \to \text{Cocycle}(K,L,n) \quad\text{when } n'+a=n.$$$

Lean4

/-- The map `Cocycle (K⟦a⟧) L n' → Cocycle K L n` when `n + a = n'`. -/
@[simps!]
def leftUnshift {n' a : ℤ} (γ : Cocycle (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : Cocycle K L n :=
  Cocycle.mk (γ.1.leftUnshift n hn) _ rfl
    (by rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl, δ_eq_zero, Cochain.leftUnshift_zero, smul_zero])

Похожие утверждения