Documentation

Mathlib.RingTheory.WittVector.DiscreteValuationRing

Witt vectors over a perfect ring #

This file establishes that Witt vectors over a perfect field are a discrete valuation ring. When k is a perfect ring, a nonzero a : ๐•Ž k can be written as p^m * b for some m : โ„• and b : ๐•Ž k with nonzero 0th coefficient. When k is also a field, this b can be chosen to be a unit of ๐•Ž k.

Main declarations #

def WittVector.succNthValUnits {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (n : โ„•) (a : kหฃ) (A : WittVector p k) (bs : Fin (n + 1) โ†’ k) :
k

This is the n+1st coefficient of our inverse.

Equations
Instances For
    @[irreducible]
    noncomputable def WittVector.inverseCoeff {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] (a : kหฃ) (A : WittVector p k) :
    โ„• โ†’ k

    Recursively defines the sequence of coefficients for the inverse to a Witt vector whose first entry is a unit.

    Equations
    Instances For
      def WittVector.mkUnit {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] {a : kหฃ} {A : WittVector p k} (hA : A.coeff 0 = โ†‘a) :

      Upgrade a Witt vector A whose first entry A.coeff 0 is a unit to be, itself, a unit in ๐•Ž k.

      Equations
      Instances For
        @[simp]
        theorem WittVector.coe_mkUnit {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] {a : kหฃ} {A : WittVector p k} (hA : A.coeff 0 = โ†‘a) :
        โ†‘(WittVector.mkUnit hA) = A
        theorem WittVector.isUnit_of_coeff_zero_ne_zero {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] (x : WittVector p k) (hx : x.coeff 0 โ‰  0) :
        theorem WittVector.irreducible (p : โ„•) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] :
        Irreducible โ†‘p
        theorem WittVector.exists_eq_pow_p_mul {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (a : WittVector p k) (ha : a โ‰  0) :
        โˆƒ (m : โ„•) (b : WittVector p k), b.coeff 0 โ‰  0 โˆง a = โ†‘p ^ m * b
        theorem WittVector.exists_eq_pow_p_mul' {p : โ„•} [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [PerfectRing k p] (a : WittVector p k) (ha : a โ‰  0) :
        โˆƒ (m : โ„•) (b : (WittVector p k)หฃ), a = โ†‘p ^ m * โ†‘b

        The ring of Witt Vectors of a perfect field of positive characteristic is a DVR.