leftShift — Mathlib

English

For any z and Φ additive, δ(n,m)(z.map Φ) equals (δ(n,m) z).map Φ.

Русский

Для любого z и Φ аддитивного, δ(n,m)(z.map Φ) = (δ(n,m) z).map Φ.

LaTeX

$$$\\delta(n,m)(z.map\\;\\Phi) = (\\delta(n,m) z).map\\;\\Phi.$$$

Lean4

/-- The map `Cochain K L n → Cochain (K⟦a⟧) L n'` when `n + a = n'`. -/
def leftShift (a n' : ℤ) (hn' : n + a = n') : Cochain (K⟦a⟧) L n' :=
  Cochain.mk
    (fun p q hpq =>
      (a * n' + ((a * (a - 1)) / 2)).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) rfl).hom ≫ γ.v (p + a) q (by cutsat))

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