The ring of Witt vectors is p-torsion free and p-adically complete

In this file, we prove that the ring of Witt vectors 𝕎 k is p-torsion free and p-adically complete when k is a perfect ring of characteristic p.

Main declarations

• WittVector.eq_zero_of_p_mul_eq_zero : If k is a perfect ring of characteristic p, then the Witt vector 𝕎 k is p-torsion free.
• isAdicCompleteIdealSpanP : If k is a perfect ring of characteristic p, then the Witt vector 𝕎 k is p-adically complete.

theorem WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] {x y : WittVector p k} {n : ℕ} : (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0

theorem WittVector.eq_zero_of_p_mul_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) (h : x * ↑p = 0) : x = 0

If k is a perfect ring of characteristic p, then the ring of Witt vectors 𝕎 k is p-torsion free.

theorem WittVector.mem_span_p_iff_coeff_zero_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) : x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0

If k is a perfect ring of characteristic p, a Witt vector x : 𝕎 k falls in ideal generated by p if and only if its zeroth coefficient is 0.

theorem WittVector.mem_span_p_pow_iff_le_coeff_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) (n : ℕ) : x ∈ Ideal.span {↑p ^ n} ↔ ∀ m < n, x.coeff m = 0

If k is a perfect ring of characteristic p, a Witt vector x : 𝕎 k falls in ideal generated by p ^ n if and only if its initial n coefficients are 0.

theorem WittVector.ker_constantCoeff {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] : RingHom.ker constantCoeff = Ideal.span {↑p}

noncomputable def WittVector.quotientPEquiv {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] : WittVector p k ⧸ Ideal.span {↑p} ≃+* k

If k is a perfect ring of characteristic p, there is an isomorphism between the quotient 𝕎 k / p and k.

@[simp]

theorem WittVector.quotientPEquiv_mk {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] (x : WittVector p k) : quotientPEquiv (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {↑p}))) x) = constantCoeff x

instance WittVector.isAdicCompleteIdealSpanP {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [CommRing k] [CharP k p] [PerfectRing k p] : IsAdicComplete (Ideal.span {↑p}) (WittVector p k)

If k is a perfect ring of characteristic p, then the ring of Witt vectors 𝕎 k is p-adically complete.