Witt structure polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

bind₁ φ (witt_polynomial p ℤ n) = bind₁ (λ i, (rename (prod.mk i) (witt_polynomial 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 witt_structure_int.

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 ℕ → mv_polynomial (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 witt_structure_int_exists_unique 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 mv_polynomial ℕ ℚ. We therefore obtain a family of polynomials witt_structure_rat Φ for every Φ : mv_polynomial idx ℚ.

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

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

Main results #

• witt_structure_rat Φ: the family of polynomials ℕ → mv_polynomial (idx × ℕ) ℚ associated with Φ : mv_polynomial idx ℚ and satisfying the property explained above.
• witt_structure_rat_prop: the proof that witt_structure_rat indeed satisfies the property.
• witt_structure_int Φ: the family of polynomials ℕ → mv_polynomial (idx × ℕ) ℤ associated with Φ : mv_polynomial idx ℤ and satisfying the property explained above.
• map_witt_structure_int: the proof that the integral polynomials with_structure_int Φ are equal to witt_structure_rat Φ when mapped to polynomials with rational coefficients.
• witt_structure_int_prop: the proof that witt_structure_int indeed satisfies the property.
• Five families of polynomials that will be used to define the ring structure on the ring of Witt vectors:
  • witt_vector.witt_zero
  • witt_vector.witt_one
  • witt_vector.witt_add
  • witt_vector.witt_mul
  • witt_vector.witt_neg (We also define witt_vector.witt_sub, and later we will prove that it describes subtraction, which is defined as λ a b, a + -b. See witt_vector.sub_coeff for this proof.)

References #

• Hazewinkel, Witt Vectors

• Commelin and Lewis, Formalizing the Ring of Witt Vectors