English
If k is a perfect ring of characteristic p, then the Witt vectors 𝕎k are complete with respect to the p‑adic topology.
Русский
Если k — совершенное кольцо характерp p, то Witt‑вектора 𝕎k полно по p‑адической топологии.
LaTeX
$$$𝕎 k \text{ is } p\\text{-adically complete}$$$
Lean4
/-- If `k` is a perfect ring of characteristic `p`, then the ring of Witt vectors `𝕎 k`
is `p`-adically complete.
-/
instance isAdicCompleteIdealSpanP : IsAdicComplete (Ideal.span {(p : 𝕎 k)}) (𝕎 k)
where
haus' := by
intro _ h
ext n
simp only [smul_eq_mul, Ideal.mul_top] at h
have := h (n + 1)
simp only [Ideal.span_singleton_pow, SModEq.zero, mem_span_p_pow_iff_le_coeff_eq_zero] at this
simpa using this n
prec' := by
intro x h
use .mk p (fun n ↦ (x (n + 1)).coeff n)
intro n
simp only [Ideal.span_singleton_pow, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
mem_span_p_pow_iff_le_coeff_eq_zero, ← le_coeff_eq_iff_le_sub_coeff_eq_zero] at h ⊢
intro i hi
exact (h hi i (Nat.lt_succ_self i)).symm
