shift — Mathlib

English

The shift operation on cocycles moves both factors K and L by a fixed integer a, producing a cocycle on the shifted complexes with the same degree n.

Русский

Сдвиг кокцикла переносит и K, и L на фиксированное целое a, порождая кокцикл на сдвинутых комплексах с тем же степенью n.

LaTeX

$$$\mathrm{shift}: \text{Cocycle}(K,L,n) \to \text{Cocycle}(K⟦a⟧,L⟦a⟧,n).$$$

Lean4

/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) (L⟦a⟧) n`. -/
@[simps!]
def shift (γ : Cocycle K L n) (a : ℤ) : Cocycle (K⟦a⟧) (L⟦a⟧) n :=
  Cocycle.mk (γ.1.shift a) _ rfl (by simp only [Cochain.δ_shift, δ_eq_zero, Cochain.shift_zero, smul_zero])

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