# Documentation

Mathlib.RingTheory.WittVector.StructurePolynomial

# 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.)
• [Hazewinkel, Witt Vectors][Haze09]

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