Witt vectors over a perfect ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

witt_vector.exists_eq_pow_p_mul: the existence of this element b over a perfect ring
witt_vector.exists_eq_pow_p_mul': the existence of this unit b over a perfect field
witt_vector.discrete_valuation_ring: 𝕎 k is a discrete valuation ring if k is a perfect field

source

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) :

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

Equations

witt_vector.succ_nth_val_units n a A bs = -↑(a⁻¹ ^ p ^ (n + 1)) * (A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + witt_vector.nth_remainder p n (witt_vector.truncate_fun (n + 1) A) bs)

source

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) :

ℕ → k

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

Equations

witt_vector.inverse_coeff a A (n + 1) = witt_vector.succ_nth_val_units n a A (λ (i : fin (n + 1)), witt_vector.inverse_coeff a A i.val)
witt_vector.inverse_coeff a A 0 = ↑a⁻¹

source

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) :

(witt_vector p k)ˣ

Upgrade a Witt vector A whose first entry A.coeff 0 is a unit to be, itself, a unit in 𝕎 k.

Equations

witt_vector.mk_unit hA = units.mk_of_mul_eq_one A {coeff := witt_vector.inverse_coeff a A} _

source

@[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) :

↑(witt_vector.mk_unit hA) = A

source

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) :

is_unit x

source

theorem witt_vector.irreducible (p : ℕ) [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] :

irreducible ↑p

source

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

source

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

source

theorem witt_vector.discrete_valuation_ring {p : ℕ} [hp : fact (nat.prime p)] {k : Type u_1} [field k] [char_p k p] [perfect_ring k p] :

discrete_valuation_ring (witt_vector p k)

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