ghostMap — Mathlib

English

Applying ghostMap to x and evaluating at n yields the nth ghost component.

Русский

Применение ghostMap к x и вычисление на n дает n-ую ghost-компоненту.

LaTeX

$$$ ghostMap\\, x\\, n = ghostComponent\\, n\\, x$$$

Lean4

/-- `WittVector.ghostMap` is a ring homomorphism that maps each Witt vector
to the sequence of its ghost components. -/
def ghostMap : 𝕎 R →+* ℕ → R where
  toFun := ghostFun
  map_zero' := ghostFun_zero
  map_one' := ghostFun_one
  map_add' := ghostFun_add
  map_mul' := ghostFun_mul

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