map — Mathlib

English

ghostMap is a ring homomorphism sending a Witt vector to its ghost components sequence.

Русский

ghostMap является гомоморфизмом кольца, отправляющим Witt-вектор в последовательность его ghost-компонент.

LaTeX

$$$\\mathrm{ghostMap} : 𝕎R \\to^+* (\\mathbb{N} \\to R)$$$

Lean4

/-- `WittVector.map f` is the ring homomorphism `𝕎 R →+* 𝕎 S` naturally induced
by a ring homomorphism `f : R →+* S`. It acts coefficientwise. -/
noncomputable def map (f : R →+* S) : 𝕎 R →+* 𝕎 S
    where
  toFun := mapFun f
  map_zero' := mapFun.zero f
  map_one' := mapFun.one f
  map_add' := mapFun.add f
  map_mul' := mapFun.mul f

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