mathlib documentation

ring_theory.witt_vector.discrete_valuation_ring

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 #

noncomputable def witt_vector.succ_nth_val_units {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] (n : β„•) (a : kΛ£) (A : witt_vector p k) (bs : fin (n + 1) β†’ k) :
k

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

Equations
noncomputable def witt_vector.inverse_coeff {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] (a : kΛ£) (A : witt_vector p k) :

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

Equations
noncomputable def witt_vector.mk_unit {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] {a : kΛ£} {A : witt_vector 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
@[simp]
theorem witt_vector.coe_mk_unit {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] {a : kΛ£} {A : witt_vector p k} (hA : A.coeff 0 = ↑a) :
theorem witt_vector.is_unit_of_coeff_zero_ne_zero {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] (x : witt_vector p k) (hx : x.coeff 0 β‰  0) :
theorem witt_vector.irreducible (p : β„•) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] :
theorem witt_vector.exists_eq_pow_p_mul {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [comm_ring k] [char_p k p] [perfect_ring k p] (a : witt_vector p k) (ha : a β‰  0) :
βˆƒ (m : β„•) (b : witt_vector p k), b.coeff 0 β‰  0 ∧ a = ↑p ^ m * b
theorem witt_vector.exists_eq_pow_p_mul' {p : β„•} [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [perfect_ring k p] (a : witt_vector p k) (ha : a β‰  0) :
βˆƒ (m : β„•) (b : (witt_vector p k)Λ£), a = ↑p ^ m * ↑b

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