Witt vectors #
In this file we define the type of p
-typical Witt vectors and ring operations on it.
The ring axioms are verified in RingTheory.WittVector.Basic
.
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 StructurePolynomial.lean
.
The n
th value of the sum of two Witt vectors can depend on the 0
-th through n
th values
of the summands. This effectively simulates a βcarryingβ operation.
Main definitions #
witt_vector p R
: the type ofp
-typical Witt vectors with coefficients inR
.witt_vector.coeff x n
: projects then
th value of the Witt vectorx
.
Notation #
We use notation π R
, entered \bbW
, for the Witt vectors over R
.
References #
-
[Hazewinkel, Witt Vectors][Haze09]
-
[Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]
- mk' :: (
- coeff : β β R
x.coeff n
is then
th coefficient of the Witt vectorx
.This concept does not have a standard name in the literature.
- )
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]
.
Instances For
Construct a Witt vector mk p x : π R
from a sequence x
of elements of R
.
Instances For
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.
Instances For
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 n
th 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β
.