rightUnshift — Mathlib

English

There is a canonical operation that, given a cocycle on K and L⟦a⟧, returns a cocycle on K and L provided that the degrees satisfy n' + a = n. This unshifts the target by a.

Русский

Существует каноническая операция, которая задана для кокцикла на K и L⟦a⟧, возвращает кокцикл на K и L при условии n' + a = n, то есть снимает сдвиг цели на a.

LaTeX

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

Lean4

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

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