frobenius_verschiebung — Mathlib

English

On Witt vectors over Z/pZ, Verschiebung is multiplication by p; Frobenius followed by Verschiebung equals p times identity.

Русский

На Witt-векторах над Z/pZ Verschiebung равна умножению на p; Фробениус, затем Verschiebung равен p-умножению на тождество.

LaTeX

$$verschiebung_zmod x = x * p and frobenius(verschiebung x) = x * p$$

Lean4

/-- The composition of Frobenius and Verschiebung is multiplication by `p`. -/
theorem frobenius_verschiebung (x : 𝕎 R) : frobenius (verschiebung x) = x * p :=
  by
  have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
    IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
  have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
  ghost_calc x
  ghost_simp [mul_comm]

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