English
The Frobenius endomorphism on Witt vectors equals the map induced by Frobenius on the base ring when applied to Witt vectors.
Русский
Эндоморфизм Frobenius на Witt-векторах равен отображению, индуцированному Frobenius на базовом кольце, при работе с Witt-векторами.
LaTeX
$$$\operatorname{frobenius} = \operatorname{map}(\operatorname{frobenius}_{R,p})$ as End(WittVectors).$$
Lean4
/-- If `R` has characteristic `p`, then there is a ring endomorphism
that raises `r : R` to the power `p`.
By applying `WittVector.map` to this endomorphism,
we obtain a ring endomorphism `frobenius R p : 𝕎 R →+* 𝕎 R`.
The underlying function of this morphism is `WittVector.frobeniusFun`.
-/
def frobenius : 𝕎 R →+* 𝕎 R where
toFun := frobeniusFun
map_zero' :=
by
refine
IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.zeroIsPoly))
(IsPoly.comp (hg := WittVector.zeroIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0
simp only [Function.comp_apply, map_zero, forall_const]
ghost_simp
map_one' :=
by
refine
IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.oneIsPoly))
(IsPoly.comp (hg := WittVector.oneIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0
simp only [Function.comp_apply, map_one, forall_const]
ghost_simp
map_add' := by ghost_calc _ _; ghost_simp
map_mul' := by ghost_calc _ _; ghost_simp
