mathlibdocumentation

ring_theory.witt_vector.structure_polynomial

Witt structure polynomials #

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