Witt vectors over a domain #
This file builds to the proof WittVector.instIsDomain
,
an instance that says if R
is an integral domain, then so is 𝕎 R
.
It depends on the API around iterated applications
of WittVector.verschiebung
and WittVector.frobenius
found in Identities.lean
.
The proof sketch
goes as follows:
any nonzero WittVector.verschiebung_nonzero
).
Known identities (WittVector.iterate_verschiebung_mul
) allow us to transform
the product of two such
Main declarations #
WittVector.iterate_verschiebung_mul_coeff
: an identity from [Haze09]WittVector.instIsDomain
WittVector.verschiebung
translates the entries of a Witt vector upward, inserting 0s in the gaps.
WittVector.shift
does the opposite, removing the first entries.
This is mainly useful as an auxiliary construction for WittVector.verschiebung_nonzero
.
Instances For
Witt vectors over a domain #
If R
is an integral domain, then so is 𝕎 R
.
This argument is adapted from
https://math.stackexchange.com/questions/4117247/ring-of-witt-vectors-over-an-integral-domain/4118723#4118723.
Equations
- ⋯ = ⋯