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 vectorstruncated_witt_vector.comm_ring
: the ring structure on truncated Witt vectorswitt_vector.truncate
: the quotient homomorphism that truncates a Witt vector, to obtain a truncated Witt vectortruncated_witt_vector.truncate
: the homomorphism that truncates a truncated Witt vector of lengthn
to one of lengthm
(for somem ≤ 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
References #
A truncated Witt vector over R
is a vector of elements of R
,
i.e., the first n
coefficients of a Witt vector.
We will define operations on this type that are compatible with the (untruncated) Witt
vector operations.
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.)
Equations
- truncated_witt_vector p n R = (fin n → R)
Instances for truncated_witt_vector
- truncated_witt_vector.inhabited
- truncated_witt_vector.has_zero
- truncated_witt_vector.has_one
- truncated_witt_vector.has_nat_cast
- truncated_witt_vector.has_int_cast
- truncated_witt_vector.has_add
- truncated_witt_vector.has_mul
- truncated_witt_vector.has_neg
- truncated_witt_vector.has_sub
- truncated_witt_vector.has_nat_scalar
- truncated_witt_vector.has_int_scalar
- truncated_witt_vector.has_nat_pow
- truncated_witt_vector.comm_ring
- truncated_witt_vector.fintype
Equations
- truncated_witt_vector.inhabited p n R = {default := λ (_x : fin n), inhabited.default}
Create a truncated_witt_vector
from a vector x
.
Equations
- truncated_witt_vector.mk p x = x
x.coeff i
is the i
th entry of x
.
Equations
- truncated_witt_vector.coeff i x = x i
We can turn a truncated Witt vector x
into a Witt vector
by setting all coefficients after x
to be 0.
truncate_fun n x
uses the first n
entries of x
to construct a truncated_witt_vector
,
which has the same base p
as x
.
This function is bundled into a ring homomorphism in witt_vector.truncate
Equations
- witt_vector.truncate_fun n x = truncated_witt_vector.mk p (λ (i : fin n), x.coeff ↑i)
Equations
- truncated_witt_vector.has_zero p n R = {zero := witt_vector.truncate_fun n 0}
Equations
- truncated_witt_vector.has_one p n R = {one := witt_vector.truncate_fun n 1}
Equations
- truncated_witt_vector.has_nat_cast p n R = {nat_cast := λ (i : ℕ), witt_vector.truncate_fun n ↑i}
Equations
- truncated_witt_vector.has_int_cast p n R = {int_cast := λ (i : ℤ), witt_vector.truncate_fun n ↑i}
Equations
- truncated_witt_vector.has_add p n R = {add := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out + y.out)}
Equations
- truncated_witt_vector.has_mul p n R = {mul := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out * y.out)}
Equations
- truncated_witt_vector.has_neg p n R = {neg := λ (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (-x.out)}
Equations
- truncated_witt_vector.has_sub p n R = {sub := λ (x y : truncated_witt_vector p n R), witt_vector.truncate_fun n (x.out - y.out)}
Equations
- truncated_witt_vector.has_nat_scalar p n R = {smul := λ (m : ℕ) (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (m • x.out)}
Equations
- truncated_witt_vector.has_int_scalar p n R = {smul := λ (m : ℤ) (x : truncated_witt_vector p n R), witt_vector.truncate_fun n (m • x.out)}
Equations
- truncated_witt_vector.has_nat_pow p n R = {pow := λ (x : truncated_witt_vector p n R) (m : ℕ), witt_vector.truncate_fun n (x.out ^ m)}
Equations
- truncated_witt_vector.comm_ring p n R = function.surjective.comm_ring (witt_vector.truncate_fun n) _ _ _ _ _ _ _ _ _ _ _ _
truncate n
is a ring homomorphism that truncates x
to its first n
entries
to obtain a truncated_witt_vector
, which has the same base p
as x
.
Equations
- witt_vector.truncate n = {to_fun := witt_vector.truncate_fun n R, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
A ring homomorphism that truncates a truncated Witt vector of length m
to
a truncated Witt vector of length n
, for n ≤ m
.
Equations
Given a family fₖ : S → truncated_witt_vector p k R
and s : S
, we produce a Witt vector by
defining the k
th entry to be the final entry of fₖ s
.
Equations
- witt_vector.lift_fun f s = {coeff := λ (k : ℕ), truncated_witt_vector.coeff (fin.last k) (⇑(f (k + 1)) s)}
Given compatible ring homs from S
into truncated_witt_vector n
for each n
, we can lift these
to a ring hom S → 𝕎 R
.
lift
defines the universal property of 𝕎 R
as the inverse limit of truncated_witt_vector n
.
Equations
- witt_vector.lift f f_compat = {to_fun := witt_vector.lift_fun f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
The uniqueness part of the universal property of 𝕎 R
.
The universal property of 𝕎 R
as projective limit of truncated Witt vector rings.
Equations
- witt_vector.lift_equiv = {to_fun := λ (f : {f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (truncated_witt_vector.truncate hk).comp (f k₂) = f k₁}), witt_vector.lift f.val _, inv_fun := λ (g : S →+* witt_vector p R), ⟨λ (k : ℕ), (witt_vector.truncate k).comp g, _⟩, left_inv := _, right_inv := _}