mathlib documentation

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

Main results

def witt_structure_rat (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) :

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

bind₁ (witt_structure_rat p Φ) (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 witt_structure_rat Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

See witt_structure_rat_prop for this property, and witt_structure_rat_exists_unique for the fact that witt_structure_rat 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 witt_structure_int for the version with integral coefficients, and map_witt_structure_int for the fact that it is equal to witt_structure_rat when mapped to polynomials over the rationals.

Equations
theorem witt_structure_rat_exists_unique (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) :

theorem witt_structure_rat_rec_aux (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) :
(witt_structure_rat p Φ n) * mv_polynomial.C (p ^ n) = (mv_polynomial.bind₁ (λ (b : idx), (mv_polynomial.rename (λ (i : ), (b, i))) (witt_polynomial p n))) Φ - ∑ (i : ) in finset.range n, (mv_polynomial.C (p ^ i)) * witt_structure_rat p Φ i ^ p ^ (n - i)

theorem witt_structure_rat_rec (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) :
witt_structure_rat p Φ n = (mv_polynomial.C (1 / p ^ n)) * ((mv_polynomial.bind₁ (λ (b : idx), (mv_polynomial.rename (λ (i : ), (b, i))) (witt_polynomial p n))) Φ - ∑ (i : ) in finset.range n, (mv_polynomial.C (p ^ i)) * witt_structure_rat p Φ i ^ p ^ (n - i))

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

def witt_structure_int (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) :

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

bind₁ (witt_structure_int p Φ) (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 witt_structure_int Φ is the same as evaluating Φ on the (appropriately renamed) n-th Witt polynomials.

See witt_structure_int_prop for this property, and witt_structure_int_exists_unique for the fact that witt_structure_int gives the unique family of polynomials with this property.

Equations
theorem C_p_pow_dvd_bind₁_rename_witt_polynomial_sub_sum {p : } {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) (IH : ∀ (m : ), m < n(mv_polynomial.map (int.cast_ring_hom )) (witt_structure_int p Φ m) = witt_structure_rat p ((mv_polynomial.map (int.cast_ring_hom )) Φ) m) :
mv_polynomial.C (p ^ n) (mv_polynomial.bind₁ (λ (b : idx), (mv_polynomial.rename (λ (i : ), (b, i))) (witt_polynomial p n))) Φ - ∑ (i : ) in finset.range n, (mv_polynomial.C (p ^ i)) * witt_structure_int p Φ i ^ p ^ (n - i)

theorem eq_witt_structure_int (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (φ : mv_polynomial (idx × ) ) (h : ∀ (n : ), (mv_polynomial.bind₁ φ) (witt_polynomial p n) = (mv_polynomial.bind₁ (λ (i : idx), (mv_polynomial.rename (prod.mk i)) (witt_polynomial p n))) Φ) :

theorem witt_structure_int_exists_unique (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) :

theorem witt_structure_prop (p : ) {R : Type u_1} {idx : Type u_2} [comm_ring R] [hp : fact (nat.prime p)] (Φ : mv_polynomial idx ) (n : ) :

theorem witt_structure_int_rename (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] {σ : Type u_1} (Φ : mv_polynomial idx ) (f : idx → σ) (n : ) :

theorem witt_structure_rat_vars (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] [fintype idx] (Φ : mv_polynomial idx ) (n : ) :

theorem witt_structure_int_vars (p : ) {idx : Type u_2} [hp : fact (nat.prime p)] [fintype idx] (Φ : mv_polynomial idx ) (n : ) :