Witt polynomials

To endow WittVector p R with a ring structure, we need to study the so-called Witt polynomials.

Fix a base value p : ℕ. The p-adic Witt polynomials are an infinite family of polynomials indexed by a natural number n, taking values in an arbitrary ring R. The variables of these polynomials are represented by natural numbers. The variable set of the nth Witt polynomial contains at most n+1 elements {0, ..., n}, with exactly these variables when R has characteristic 0.

These polynomials are used to define the addition and multiplication operators on the type of Witt vectors. (While this type itself is not complicated, the ring operations are what make it interesting.)

When the base p is invertible in R, the p-adic Witt polynomials form a basis for MvPolynomial ℕ R, equivalent to the standard basis.

Main declarations

• WittPolynomial p R n: the n-th Witt polynomial, viewed as polynomial over the ring R
• xInTermsOfW p R n: if p is invertible, the polynomial X n is contained in the subalgebra generated by the Witt polynomials. xInTermsOfW p R n is the explicit polynomial, which upon being bound to the Witt polynomials yields X n.
• bind₁_wittPolynomial_xInTermsOfW: the proof of the claim that bind₁ (xInTermsOfW p R) (W_ R n) = X n
• bind₁_xInTermsOfW_wittPolynomial: the converse of the above statement

Notation

In this file we use the following notation

• p is a natural number, typically assumed to be prime.
• R and S are commutative rings
• W n (and W_ R n when the ring needs to be explicit) denotes the nth Witt polynomial

References

• [Hazewinkel, Witt Vectors][Haze09]

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

noncomputable def wittPolynomial (p : ℕ) (R : Type u_1) [CommRing R] (n : ℕ) : MvPolynomial ℕ R

wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Equations

• wittPolynomial p R n = Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => (MvPolynomial.monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)

theorem wittPolynomial_eq_sum_C_mul_X_pow (p : ℕ) (R : Type u_1) [CommRing R] (n : ℕ) : wittPolynomial p R n = Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * MvPolynomial.X i ^ p ^ (n - i)

We set up notation locally to this file, to keep statements short and comprehensible. This allows us to simply write W n or W_ ℤ n.

def Witt.termW_ : Lean.ParserDescr

wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Equations

• Witt.termW_ = Lean.ParserDescr.node `Witt.termW_ 1024 (Lean.ParserDescr.symbol "W_")

def Witt.termW : Lean.ParserDescr

wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as:

∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Equations

• Witt.termW = Lean.ParserDescr.node `Witt.termW 1024 (Lean.ParserDescr.symbol "W")

The first observation is that the Witt polynomial doesn't really depend on the coefficient ring. If we map the coefficients through a ring homomorphism, we obtain the corresponding Witt polynomial over the target ring.

@[simp]

theorem map_wittPolynomial (p : ℕ) {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (n : ℕ) : (MvPolynomial.map f) (wittPolynomial p R n) = wittPolynomial p S n

@[simp]

theorem constantCoeff_wittPolynomial (p : ℕ) (R : Type u_1) [CommRing R] [hp : Fact (Nat.Prime p)] (n : ℕ) : MvPolynomial.constantCoeff (wittPolynomial p R n) = 0

@[simp]

theorem wittPolynomial_zero (p : ℕ) (R : Type u_1) [CommRing R] : wittPolynomial p R 0 = MvPolynomial.X 0

@[simp]

theorem wittPolynomial_one (p : ℕ) (R : Type u_1) [CommRing R] : wittPolynomial p R 1 = MvPolynomial.C ↑p * MvPolynomial.X 1 + MvPolynomial.X 0 ^ p

theorem aeval_wittPolynomial (p : ℕ) (R : Type u_1) [CommRing R] {A : Type u_3} [CommRing A] [Algebra R A] (f : ℕ → A) (n : ℕ) : (MvPolynomial.aeval f) (wittPolynomial p R n) = Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => ↑p ^ i * f i ^ p ^ (n - i)

@[simp]

theorem wittPolynomial_zmod_self (p : ℕ) (n : ℕ) : wittPolynomial p (ZMod (p ^ (n + 1))) (n + 1) = (MvPolynomial.expand p) (wittPolynomial p (ZMod (p ^ (n + 1))) n)

Over the ring ZMod (p^(n+1)), we produce the n+1st Witt polynomial by expanding the nth Witt polynomial by p.

theorem wittPolynomial_vars (p : ℕ) (R : Type u_1) [CommRing R] [hp : NeZero p] [CharZero R] (n : ℕ) : MvPolynomial.vars (wittPolynomial p R n) = Finset.range (n + 1)

theorem wittPolynomial_vars_subset (p : ℕ) (R : Type u_1) [CommRing R] [hp : NeZero p] (n : ℕ) : MvPolynomial.vars (wittPolynomial p R n) ⊆ Finset.range (n + 1)

Witt polynomials as a basis of the polynomial algebra

If p is invertible in R, then the Witt polynomials form a basis of the polynomial algebra MvPolynomial ℕ R. The polynomials xInTermsOfW give the coordinate transformation in the backwards direction.

noncomputable def xInTermsOfW (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] : ℕ → MvPolynomial ℕ R

The xInTermsOfW p R n is the polynomial on the basis of Witt polynomials that corresponds to the ordinary X n.

Equations

• One or more equations did not get rendered due to their size.

theorem xInTermsOfW_eq (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] {n : ℕ} : xInTermsOfW p R n = (MvPolynomial.X n - Finset.sum (Finset.range n) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * MvPolynomial.C (⅟↑p ^ n)

@[simp]

theorem constantCoeff_xInTermsOfW (p : ℕ) (R : Type u_1) [CommRing R] [hp : Fact (Nat.Prime p)] [Invertible ↑p] (n : ℕ) : MvPolynomial.constantCoeff (xInTermsOfW p R n) = 0

@[simp]

theorem xInTermsOfW_zero (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] : xInTermsOfW p R 0 = MvPolynomial.X 0

theorem xInTermsOfW_vars_aux (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : n ∈ MvPolynomial.vars (xInTermsOfW p ℚ n) ∧ MvPolynomial.vars (xInTermsOfW p ℚ n) ⊆ Finset.range (n + 1)

theorem xInTermsOfW_vars_subset (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : MvPolynomial.vars (xInTermsOfW p ℚ n) ⊆ Finset.range (n + 1)

theorem xInTermsOfW_aux (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] (n : ℕ) : xInTermsOfW p R n * MvPolynomial.C (↑p ^ n) = MvPolynomial.X n - Finset.sum (Finset.range n) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

@[simp]

theorem bind₁_xInTermsOfW_wittPolynomial (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] (k : ℕ) : (MvPolynomial.bind₁ (xInTermsOfW p R)) (wittPolynomial p R k) = MvPolynomial.X k

@[simp]

theorem bind₁_wittPolynomial_xInTermsOfW (p : ℕ) (R : Type u_1) [CommRing R] [Invertible ↑p] (n : ℕ) : (MvPolynomial.bind₁ (wittPolynomial p R)) (xInTermsOfW p R n) = MvPolynomial.X n