Witt vectors #
This file verifies that the ring operations on witt_vector p R
satisfy the axioms of a commutative ring.
Main definitions #
witt_vector.map
: lifts a ring homomorphismR →+* S
to a ring homomorphism𝕎 R →+* 𝕎 S
.witt_vector.ghost_component n x
: evaluates then
th Witt polynomial on the firstn
coefficients ofx
, producing a value inR
. This is a ring homomorphism.witt_vector.ghost_map
: 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
.witt_vector.comm_ring
: 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 #
f : α → β
induces a map from 𝕎 α
to 𝕎 β
by applying f
componentwise.
If f
is a ring homomorphism, then so is f
, see witt_vector.map f
.
Equations
- witt_vector.map_fun f = λ (x : witt_vector p α), {coeff := f ∘ x.coeff}
The commutative ring structure on 𝕎 R
.
Equations
- witt_vector.comm_ring p R = function.surjective.comm_ring (witt_vector.map_fun ⇑(mv_polynomial.counit R)) _ _ _ _ _ _ _ _ _ _ _ _
witt_vector.map f
is the ring homomorphism 𝕎 R →+* 𝕎 S
naturally induced
by a ring homomorphism f : R →+* S
. It acts coefficientwise.
Equations
- witt_vector.map f = {to_fun := witt_vector.map_fun ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
witt_vector.ghost_map
is a ring homomorphism that maps each Witt vector
to the sequence of its ghost components.
Evaluates the n
th Witt polynomial on the first n
coefficients of x
,
producing a value in R
.
Equations
- witt_vector.ghost_component n = (pi.eval_ring_hom (λ (n : ℕ), R) n).comp witt_vector.ghost_map
witt_vector.ghost_map
is a ring isomorphism when p
is invertible in R
.
witt_vector.coeff x 0
as a ring_hom
Equations
- witt_vector.constant_coeff = {to_fun := λ (x : witt_vector p R), x.coeff 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}