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 (Nat.Prime p)] : ℕ → ℕ → MvPolynomial ℕ ℤ

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

• WittVector.wittMulN p 0 = 0
• WittVector.wittMulN p n.succ = fun (k : ℕ) => (MvPolynomial.bind₁ (Function.uncurry ![WittVector.wittMulN p n, MvPolynomial.X])) (WittVector.wittAdd p k)

theorem WittVector.mulN_coeff {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ℕ) (x : WittVector p R) (k : ℕ) : (x * ↑n).coeff k = (MvPolynomial.aeval x.coeff) (WittVector.wittMulN p n k)

theorem WittVector.mulN_isPoly (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : WittVector.IsPoly p fun (R : Type u_2) (_Rcr : CommRing R) (x : WittVector p R) => x * ↑n

Multiplication by n is a polynomial function.

@[simp]

theorem WittVector.bind₁_wittMulN_wittPolynomial (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (k : ℕ) : (MvPolynomial.bind₁ (WittVector.wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k