Witt structure polynomials

In this file we prove the main theorem that makes the whole theory of Witt vectors work. Briefly, consider a polynomial Φ : MvPolynomial idx ℤ over the integers, with polynomials variables indexed by an arbitrary type idx.

Then there exists a unique family of polynomials φ : ℕ → MvPolynomial (idx × ℕ) Φ such that for all n : ℕ we have (wittStructureInt_existsUnique)

bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℤ n))) Φ

In other words: evaluating the n-th Witt polynomial on the family φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

N.b.: As far as we know, these polynomials do not have a name in the literature, so we have decided to call them the “Witt structure polynomials”. See wittStructureInt.

Special cases

With the main result of this file in place, we apply it to certain special polynomials. For example, by taking Φ = X tt + X ff resp. Φ = X tt * X ff we obtain families of polynomials witt_add resp. witt_mul (with type ℕ → MvPolynomial (Bool × ℕ) ℤ) that will be used in later files to define the addition and multiplication on the ring of Witt vectors.

Outline of the proof

The proof of wittStructureInt_existsUnique is rather technical, and takes up most of this file.

We start by proving the analogous version for polynomials with rational coefficients, instead of integer coefficients. In this case, the solution is rather easy, since the Witt polynomials form a faithful change of coordinates in the polynomial ring MvPolynomial ℕ ℚ. We therefore obtain a family of polynomials wittStructureRat Φ for every Φ : MvPolynomial idx ℚ.

If Φ has integer coefficients, then the polynomials wittStructureRat Φ n do so as well. Proving this claim is the essential core of this file, and culminates in map_wittStructureInt, which proves that upon mapping the coefficients of wittStructureInt Φ n from the integers to the rationals, one obtains wittStructureRat Φ n. Ultimately, the proof of map_wittStructureInt relies on

dvd_sub_pow_of_dvd_sub {R : Type*} [CommRing R] {p : ℕ} {a b : R} :
    (p : R) ∣ a - b → ∀ (k : ℕ), (p : R) ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k

Main results

• wittStructureRat Φ: the family of polynomials ℕ → MvPolynomial (idx × ℕ) ℚ associated with Φ : MvPolynomial idx ℚ and satisfying the property explained above.
• wittStructureRat_prop: the proof that wittStructureRat indeed satisfies the property.
• wittStructureInt Φ: the family of polynomials ℕ → MvPolynomial (idx × ℕ) ℤ associated with Φ : MvPolynomial idx ℤ and satisfying the property explained above.
• map_wittStructureInt: the proof that the integral polynomials with_structure_int Φ are equal to wittStructureRat Φ when mapped to polynomials with rational coefficients.
• wittStructureInt_prop: the proof that wittStructureInt indeed satisfies the property.
• Five families of polynomials that will be used to define the ring structure on the ring of Witt vectors:
  • WittVector.wittZero
  • WittVector.wittOne
  • WittVector.wittAdd
  • WittVector.wittMul
  • WittVector.wittNeg (We also define WittVector.wittSub, and later we will prove that it describes subtraction, which is defined as fun a b ↦ a + -b. See WittVector.sub_coeff for this proof.)

References

• [Hazewinkel, Witt Vectors][Haze09]

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

def Witt.termW__1 : 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__1 = Lean.ParserDescr.node `Witt.termW__1 1024 (Lean.ParserDescr.symbol "W_")

def Witt.termW_1 : 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_1 = Lean.ParserDescr.node `Witt.termW_1 1024 (Lean.ParserDescr.symbol "W")

noncomputable def wittStructureRat (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ) : MvPolynomial (idx × ℕ) ℚ

wittStructureRat Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℚ that are uniquely characterised by the property that

bind₁ (wittStructureRat p Φ) (wittPolynomial p ℚ n) =
bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℚ n))) Φ

In other words: evaluating the n-th Witt polynomial on the family wittStructureRat Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

See wittStructureRat_prop for this property, and wittStructureRat_existsUnique for the fact that wittStructureRat gives the unique family of polynomials with this property.

These polynomials turn out to have integral coefficients, but it requires some effort to show this. See wittStructureInt for the version with integral coefficients, and map_wittStructureInt for the fact that it is equal to wittStructureRat when mapped to polynomials over the rationals.

Equations

• wittStructureRat p Φ n = (MvPolynomial.bind₁ fun (k : ℕ) => (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ k)) Φ) (xInTermsOfW p ℚ n)

theorem wittStructureRat_prop (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ) : (MvPolynomial.bind₁ (wittStructureRat p Φ)) (wittPolynomial p ℚ n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ n)) Φ

theorem wittStructureRat_existsUnique (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) : ∃! (φ : ℕ → MvPolynomial (idx × ℕ) ℚ), ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (wittPolynomial p ℚ n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ n)) Φ

theorem wittStructureRat_rec_aux (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ) : wittStructureRat p Φ n * MvPolynomial.C (↑p ^ n) = (MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ℕ) => (b, i)) (wittPolynomial p ℚ n)) Φ - Finset.sum (Finset.range n) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

theorem wittStructureRat_rec (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ) : wittStructureRat p Φ n = MvPolynomial.C (1 / ↑p ^ n) * ((MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ℕ) => (b, i)) (wittPolynomial p ℚ n)) Φ - Finset.sum (Finset.range n) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Write wittStructureRat p φ n in terms of wittStructureRat p φ i for i < n.

noncomputable def wittStructureInt (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) : MvPolynomial (idx × ℕ) ℤ

wittStructureInt Φ is a family of polynomials ℕ → MvPolynomial (idx × ℕ) ℤ that are uniquely characterised by the property that

bind₁ (wittStructureInt p Φ) (wittPolynomial p ℤ n) =
bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℤ n))) Φ

In other words: evaluating the n-th Witt polynomial on the family wittStructureInt Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

See wittStructureInt_prop for this property, and wittStructureInt_existsUnique for the fact that wittStructureInt gives the unique family of polynomials with this property.

Equations

• wittStructureInt p Φ n = Finsupp.mapRange Rat.num wittStructureInt.proof_1 (wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n)

theorem bind₁_rename_expand_wittPolynomial {p : ℕ} {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) (IH : ∀ m < n + 1, (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m) : (MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ℕ) => (b, i)) ((MvPolynomial.expand p) (wittPolynomial p ℤ n))) Φ = (MvPolynomial.bind₁ fun (i : ℕ) => (MvPolynomial.expand p) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n)

theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum {p : ℕ} {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) (IH : ∀ m < n, (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m) : MvPolynomial.C ↑(p ^ n) ∣ (MvPolynomial.bind₁ fun (b : idx) => (MvPolynomial.rename fun (i : ℕ) => (b, i)) (wittPolynomial p ℤ n)) Φ - Finset.sum (Finset.range n) fun (i : ℕ) => MvPolynomial.C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)

@[simp]

theorem map_wittStructureInt (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) : (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n

theorem wittStructureInt_prop (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) : (MvPolynomial.bind₁ (wittStructureInt p Φ)) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ

theorem eq_wittStructureInt (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (φ : ℕ → MvPolynomial (idx × ℕ) ℤ) (h : ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ) : φ = wittStructureInt p Φ

theorem wittStructureInt_existsUnique (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) : ∃! (φ : ℕ → MvPolynomial (idx × ℕ) ℤ), ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ

theorem witt_structure_prop (p : ℕ) {R : Type u_1} {idx : Type u_2} [CommRing R] [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ) : (MvPolynomial.aeval fun (i : ℕ) => (MvPolynomial.map (Int.castRingHom R)) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) = (MvPolynomial.aeval fun (i : idx) => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p R n)) Φ

theorem wittStructureInt_rename (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] {σ : Type u_3} (Φ : MvPolynomial idx ℤ) (f : idx → σ) (n : ℕ) : wittStructureInt p ((MvPolynomial.rename f) Φ) n = (MvPolynomial.rename (Prod.map f id)) (wittStructureInt p Φ n)

@[simp]

theorem constantCoeff_wittStructureRat_zero (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) : MvPolynomial.constantCoeff (wittStructureRat p Φ 0) = MvPolynomial.constantCoeff Φ

theorem constantCoeff_wittStructureRat (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (h : MvPolynomial.constantCoeff Φ = 0) (n : ℕ) : MvPolynomial.constantCoeff (wittStructureRat p Φ n) = 0

@[simp]

theorem constantCoeff_wittStructureInt_zero (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) : MvPolynomial.constantCoeff (wittStructureInt p Φ 0) = MvPolynomial.constantCoeff Φ

theorem constantCoeff_wittStructureInt (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (h : MvPolynomial.constantCoeff Φ = 0) (n : ℕ) : MvPolynomial.constantCoeff (wittStructureInt p Φ n) = 0

theorem wittStructureRat_vars (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [Fintype idx] (Φ : MvPolynomial idx ℚ) (n : ℕ) : MvPolynomial.vars (wittStructureRat p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)

theorem wittStructureInt_vars (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [Fintype idx] (Φ : MvPolynomial idx ℤ) (n : ℕ) : MvPolynomial.vars (wittStructureInt p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)