# Documentation

Mathlib.RingTheory.WittVector.WittPolynomial

# Witt polynomials #

To endow WittVector p R with a ring structure, we need to study the so-called Witt polynomials.

Fix a base value p : ℕ. The p-adic Witt polynomials are an infinite family of polynomials indexed by a natural number n, taking values in an arbitrary ring R. The variables of these polynomials are represented by natural numbers. The variable set of the nth Witt polynomial contains at most n+1 elements {0, ..., n}, with exactly these variables when R has characteristic 0.

These polynomials are used to define the addition and multiplication operators on the type of Witt vectors. (While this type itself is not complicated, the ring operations are what make it interesting.)

When the base p is invertible in R, the p-adic Witt polynomials form a basis for MvPolynomial ℕ R, equivalent to the standard basis.

## Main declarations #

• WittPolynomial p R n: the n-th Witt polynomial, viewed as polynomial over the ring R
• xInTermsOfW p R n: if p is invertible, the polynomial X n is contained in the subalgebra generated by the Witt polynomials. xInTermsOfW p R n is the explicit polynomial, which upon being bound to the Witt polynomials yields X n.
• bind₁_wittPolynomial_xInTermsOfW: the proof of the claim that bind₁ (xInTermsOfW p R) (W_ R n) = X n
• bind₁_xInTermsOfW_wittPolynomial: the converse of the above statement

## Notation #

In this file we use the following notation

• p is a natural number, typically assumed to be prime.
• R and S are commutative rings
• W n (and W_ R n when the ring needs to be explicit) denotes the nth Witt polynomial
• [Hazewinkel, Witt Vectors][Haze09]

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