Truncated Witt vectors #
The ring of truncated Witt vectors (of length
n) is a quotient of the ring of Witt vectors.
It retains the first
n coefficients of each Witt vector.
In this file, we set up the basic quotient API for this ring.
The ring of Witt vectors is the projective limit of all the rings of truncated Witt vectors.
Main declarations #
truncated_witt_vector: the underlying type of the ring of truncated Witt vectors
truncated_witt_vector.comm_ring: the ring structure on truncated Witt vectors
witt_vector.truncate: the quotient homomorphism that truncates a Witt vector, to obtain a truncated Witt vector
truncated_witt_vector.truncate: the homomorphism that truncates a truncated Witt vector of length
nto one of length
m ≤ n)
witt_vector.lift: the unique ring homomorphism into the ring of Witt vectors that is compatible with a family of ring homomorphisms to the truncated Witt vectors: this realizes the ring of Witt vectors as projective limit of the rings of truncated Witt vectors
A truncated Witt vector over
R is a vector of elements of
i.e., the first
n coefficients of a Witt vector.
We will define operations on this type that are compatible with the (untruncated) Witt
truncated_witt_vector p n R takes a parameter
p : ℕ that is not used in the definition.
In practice, this number
p is assumed to be a prime number,
and under this assumption we construct a ring structure on
truncated_witt_vector p n R.
truncated_witt_vector p₁ n R and
truncated_witt_vector p₂ n R are definitionally
equal as types but will have different ring operations.)
We can turn a truncated Witt vector
x into a Witt vector
by setting all coefficients after
x to be 0.
truncate n is a ring homomorphism that truncates
x to its first
to obtain a
truncated_witt_vector, which has the same base
A ring homomorphism that truncates a truncated Witt vector of length
a truncated Witt vector of length
n ≤ m.
Given a family
fₖ : S → truncated_witt_vector p k R and
s : S, we produce a Witt vector by
kth entry to be the final entry of
Given compatible ring homs from
truncated_witt_vector n for each
n, we can lift these
to a ring hom
S → 𝕎 R.
The uniqueness part of the universal property of
The universal property of
𝕎 R as projective limit of truncated Witt vector rings.