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 #
witt_vector.exists_eq_pow_p_mul
: the existence of this elementb
over a perfect ringwitt_vector.exists_eq_pow_p_mul'
: the existence of this unitb
over a perfect fieldwitt_vector.discrete_valuation_ring
:๐ k
is a discrete valuation ring ifk
is a perfect field
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โปยน
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} _
@[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
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) :
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) :
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] :
The ring of Witt Vectors of a perfect field of positive characteristic is a DVR.