instIsAdicCompleteMaximalIdeal — Mathlib

English

The maximal ideal of ℤ_p yields an adically complete ring; more precisely, (ℤ_p, maximalIdeal(ℤ_p)) is adically complete.

Русский

Максимальный идеал ℤ_p образует адическую полноту кольца; (ℤ_p, maximalIdeal(ℤ_p)) является адически полным.

LaTeX

$$IsAdicComplete(maximalIdeal(ℤ_[p]), ℤ_[p]).$$

Lean4

instance : IsAdicComplete (maximalIdeal ℤ_[p]) ℤ_[p] where
  prec' x
    hx :=
    by
    simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.sub_mem, maximalIdeal_eq_span_p,
      Ideal.span_singleton_pow, ← norm_le_pow_iff_mem_span_pow] at hx ⊢
    let x' : CauSeq ℤ_[p] norm := ⟨x, ?_⟩; swap
    · intro ε hε
      obtain ⟨m, hm⟩ := exists_pow_neg_lt p hε
      refine ⟨m, fun n hn => lt_of_le_of_lt ?_ hm⟩
      rw [← neg_sub, norm_neg]
      exact hx hn
    · refine ⟨x'.lim, fun n => ?_⟩
      have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _
      obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this
      by_cases hin : i ≤ n
      · exact (hi i le_rfl n hin).le
      · push_neg at hin
        specialize hi i le_rfl i le_rfl
        specialize hx hin.le
        have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
        rw [sub_add_sub_cancel] at this
        exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

Похожие утверждения