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 #
TruncatedWittVector: the underlying type of the ring of truncated Witt vectors
TruncatedWittVector.instCommRing: the ring structure on truncated Witt vectors
WittVector.truncate: the quotient homomorphism that truncates a Witt vector, to obtain a truncated Witt vector
TruncatedWittVector.truncate: the homomorphism that truncates a truncated Witt vector of length
nto one of length
m ≤ n)
WittVector.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
[Hazewinkel, Witt Vectors][Haze09]
[Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]
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
TruncatedWittVector 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
TruncatedWittVector p n R.
TruncatedWittVector p₁ n R and
TruncatedWittVector p₂ n R are definitionally
equal as types but will have different ring operations.)
A ring homomorphism that truncates a truncated Witt vector of length
a truncated Witt vector of length
n ≤ m.
Given a family
fₖ : S → TruncatedWittVector 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
TruncatedWittVector 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.