Witt vectors #
This file verifies that the ring operations on WittVector p R
satisfy the axioms of a commutative ring.
Main definitions #
WittVector.map
: lifts a ring homomorphismR →+* S
to a ring homomorphism𝕎 R →+* 𝕎 S
.WittVector.ghostComponent n x
: evaluates then
th Witt polynomial on the firstn
coefficients ofx
, producing a value inR
. This is a ring homomorphism.WittVector.ghostMap
: a ring homomorphism𝕎 R →+* (ℕ → R)
, obtained by packaging all the ghost components together. Ifp
is invertible inR
, then the ghost map is an equivalence, which we use to define the ring operations on𝕎 R
.WittVector.CommRing
: the ring structure induced by the ghost components.
Notation #
We use notation 𝕎 R
, entered \bbW
, for the Witt vectors over R
.
Implementation details #
As we prove that the ghost components respect the ring operations, we face a number of repetitive proofs. To avoid duplicating code we factor these proofs into a custom tactic, only slightly more powerful than a tactic macro. This tactic is not particularly useful outside of its applications in this file.
References #
-
[Hazewinkel, Witt Vectors][Haze09]
-
[Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]
f : α → β
induces a map from 𝕎 α
to 𝕎 β
by applying f
componentwise.
If f
is a ring homomorphism, then so is f
, see WittVector.map f
.
Instances For
Auxiliary tactic for showing that mapFun
respects the ring operations.
Instances For
An auxiliary tactic for proving that ghostFun
respects the ring operations.
Instances For
The commutative ring structure on 𝕎 R
.
WittVector.map f
is the ring homomorphism 𝕎 R →+* 𝕎 S
naturally induced
by a ring homomorphism f : R →+* S
. It acts coefficientwise.
Instances For
WittVector.ghostMap
is a ring homomorphism that maps each Witt vector
to the sequence of its ghost components.
Instances For
Evaluates the n
th Witt polynomial on the first n
coefficients of x
,
producing a value in R
.
Instances For
WittVector.ghostMap
is a ring isomorphism when p
is invertible in R
.
Instances For
WittVector.coeff x 0
as a RingHom