English
There is a natural Witt-vector Frobenius functor FrobeniusFun that sends a Witt vector to another Witt vector by applying the Frobenius polynomial to its coordinates.
Русский
Существует естественный функтор Фробениуса на Witt-векторах, который отправляет Witt-вектор в другой Witt-вектор, применяя полином Фробениуса к его координатам.
LaTeX
$$$\text{frobeniusFun} : 𝕎_p(R) \to 𝕎_p(R) \quad\text{defined by}\quad \operatorname{coeff}(\operatorname{frobeniusFun}(x),n) = \mathrm{aeval}_{x.coeff}(\operatorname{frobeniusPoly}(p,n)).$$$
Lean4
/-- `frobeniusFun` is the function underlying the ring endomorphism
`frobenius : 𝕎 R →+* frobenius 𝕎 R`. -/
def frobeniusFun (x : 𝕎 R) : 𝕎 R :=
mk p fun n => MvPolynomial.aeval x.coeff (frobeniusPoly p n)
