# 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 #

• WittVector.exists_eq_pow_p_mul: the existence of this element b over a perfect ring
• WittVector.exists_eq_pow_p_mul': the existence of this unit b over a perfect field
• WittVector.discreteValuationRing: ๐ k is a discrete valuation ring if k is a perfect field
def WittVector.succNthValUnits {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] (n : โ) (a : kหฃ) (A : ) (bs : Fin (n + 1) โ k) :
k

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

Equations
Instances For
noncomputable def WittVector.inverseCoeff {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] (a : kหฃ) (A : ) :
โ โ 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 p.Prime] {k : Type u_1} [] [CharP k p] {a : kหฃ} {A : } (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 p.Prime] {k : Type u_1} [] [CharP k p] {a : kหฃ} {A : } (hA : A.coeff 0 = โa) :
โ() = A
theorem WittVector.isUnit_of_coeff_zero_ne_zero {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] (x : ) (hx : x.coeff 0 โ  0) :
theorem WittVector.irreducible (p : โ) [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] :
Irreducible โp
theorem WittVector.exists_eq_pow_p_mul {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] [] (a : ) (ha : a โ  0) :
โ (m : โ) (b : ), b.coeff 0 โ  0 โง a = โp ^ m * b
theorem WittVector.exists_eq_pow_p_mul' {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] [] (a : ) (ha : a โ  0) :
โ (m : โ) (b : ()หฃ), a = โp ^ m * โb
theorem WittVector.discreteValuationRing {p : โ} [hp : Fact p.Prime] {k : Type u_1} [] [CharP k p] [] :

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