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.isDiscreteValuationRing: 𝕎 k is a discrete valuation ring if k is a perfect field

noncomputable 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

• WittVector.succNthValUnits n a A bs = -↑(a⁻¹ ^ p ^ (n + 1)) * (A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) A) bs)

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

• WittVector.inverseCoeff a A 0 = ↑a⁻¹
• WittVector.inverseCoeff a A n.succ = WittVector.succNthValUnits n a A fun (i : Fin (n + 1)) => WittVector.inverseCoeff a A ↑i

noncomputable 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) : (WittVector p k)ˣ

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

Equations

• WittVector.mkUnit hA = Units.mkOfMulEqOne A { coeff := WittVector.inverseCoeff a A } ⋯

@[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) : ↑(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) : IsUnit x

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

instance WittVector.isDiscreteValuationRing {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [PerfectRing k p] : IsDiscreteValuationRing (WittVector p k)

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