Documentation

Mathlib.RingTheory.WittVector.Domain

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 $x$ is an iterated application of $V$ to some vector $w_x$ whose 0th component is nonzero (WittVector.verschiebung_nonzero). Known identities (WittVector.iterate_verschiebung_mul) allow us to transform the product of two such $x$ and $y$ to the form $V^{m+n}\left(F^n(w_x) \cdot F^m(w_y)\right)$, the 0th component of which must be nonzero.

Main declarations #

The shift operator #

def WittVector.shift {p : } {R : Type u_1} (x : WittVector p R) (n : ) :

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.

Equations
  • x.shift n = { coeff := fun (i : ) => x.coeff (n + i) }
Instances For
    theorem WittVector.shift_coeff {p : } {R : Type u_1} (x : WittVector p R) (n : ) (k : ) :
    (x.shift n).coeff k = x.coeff (n + k)
    theorem WittVector.verschiebung_shift {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (k : ) (h : i < k + 1, x.coeff i = 0) :
    WittVector.verschiebung (x.shift k.succ) = x.shift k
    theorem WittVector.eq_iterate_verschiebung {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] {x : WittVector p R} {n : } (h : i < n, x.coeff i = 0) :
    x = (⇑WittVector.verschiebung)^[n] (x.shift n)
    theorem WittVector.verschiebung_nonzero {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] {x : WittVector p R} (hx : x 0) :
    ∃ (n : ) (x' : WittVector p R), x'.coeff 0 0 x = (⇑WittVector.verschiebung)^[n] x'

    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
    • =
    instance WittVector.instIsDomain {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [IsDomain R] :
    Equations
    • =