Documentation

Multiplication by n in the ring of Witt vectors #

In this file we show that multiplication by n in the ring of Witt vectors is a polynomial function. We then use this fact to show that the composition of Frobenius and Verschiebung is equal to multiplication by p.

Main declarations #

• mulN_isPoly: multiplication by n is a polynomial function

References #

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

noncomputable def WittVector.wittMulN (p : ) [hp : Fact p.Prime] :

wittMulN p n is the family of polynomials that computes the coefficients of x * n in terms of the coefficients of the Witt vector x.

Equations
Instances For
theorem WittVector.mulN_coeff {p : } {R : Type u_1} [hp : Fact p.Prime] [] (n : ) (x : ) (k : ) :
(x * n).coeff k = (MvPolynomial.aeval x.coeff) ()
theorem WittVector.mulN_isPoly (p : ) [hp : Fact p.Prime] (n : ) :
WittVector.IsPoly p fun (R : Type u_2) (_Rcr : ) (x : ) => x * n

Multiplication by n is a polynomial function.

@[simp]
theorem WittVector.bind₁_wittMulN_wittPolynomial (p : ) [hp : Fact p.Prime] (n : ) (k : ) :
() = n *