In this file we define the type of p-typical Witt vectors and ring operations on it.
The ring axioms are verified in ring_theory/witt_vector/basic.lean.
For a fixed commutative ring R and prime p,
a Witt vector x : 𝕎 R is an infinite sequence ℕ → R of elements of R.
However, the ring operations + and * are not defined in the obvious component-wise way.
Instead, these operations are defined via certain polynomials
using the machinery in structure_polynomial.lean.
The nth value of the sum of two Witt vectors can depend on the 0-th through nth values
of the summands. This effectively simulates a “carrying” operation.
witt_vector p R is the ring of p-typical Witt vectors over the commutative ring R,
where p is a prime number.
If p is invertible in R, this ring is isomorphic to ℕ → R (the product of ℕ copies of R).
If R is a ring of characteristic p, then witt_vector p R is a ring of characteristic 0.
The canonical example is witt_vector p (zmod p),
which is isomorphic to the p-adic integers ℤ_[p].
An auxiliary definition used in witt_vector.eval.
Evaluates a polynomial whose variables come from the disjoint union of k copies of ℕ,
with a curried evaluation x.
This can be defined more generally but we use only a specific instance here.
Let φ be a family of polynomials, indexed by natural numbers, whose variables come from the
disjoint union of k copies of ℕ, and let xᵢ be a Witt vector for 0 ≤ i < k.
eval φ x evaluates φ mapping the variable X_(i, n) to the nth coefficient of xᵢ.
Instantiating φ with certain polynomials defined in structure_polynomial.lean establishes the
ring operations on 𝕎 R. For example, witt_vector.witt_add is such a φ with k = 2;
evaluating this at (x₀, x₁) gives us the sum of two Witt vectors x₀ + x₁.