In this file we define the type of
p-typical Witt vectors and ring operations on it.
The ring axioms are verified in
For a fixed commutative ring
R and prime
a Witt vector
x : 𝕎 R is an infinite sequence
ℕ → R of elements of
However, the ring operations
* are not defined in the obvious component-wise way.
Instead, these operations are defined via certain polynomials
using the machinery in
nth value of the sum of two Witt vectors can depend on the
of the summands. This effectively simulates a “carrying” operation.
witt_vector p R: the type of
p-typical Witt vectors with coefficients in
witt_vector.coeff x n: projects the
nth value of the Witt vector
We use notation
𝕎 R, entered
\bbW, for the Witt vectors over
witt_vector p R is the ring of
p-typical Witt vectors over the commutative ring
p is a prime number.
p is invertible in
R, this ring is isomorphic to
ℕ → R (the product of
ℕ copies of
R is a ring of characteristic
witt_vector p R is a ring of characteristic
The canonical example is
witt_vector p (zmod p),
which is isomorphic to the
The polynomials used for describing the subtraction of the ring of Witt vectors.
a - b is defined as
a + -b.
witt_vector.sub_coeff for a proof that subtraction is precisely
given by these polynomials
An auxiliary definition used in
Evaluates a polynomial whose variables come from the disjoint union of
k copies of
with a curried evaluation
This can be defined more generally but we use only a specific instance here.
φ 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
φ with certain polynomials defined in
structure_polynomial.lean establishes the
ring operations on
𝕎 R. For example,
witt_vector.witt_add is such a
k = 2;
evaluating this at
(x₀, x₁) gives us the sum of two Witt vectors
x₀ + x₁.