adic_module_basis — Mathlib

English

For an ideal I of R and an R-module M, the family I^n M forms a basis for the adic topology on M.

Русский

Для идеала I в кольце R и модуля M семейство I^n M образует базис адической топологии на M.

LaTeX

$$$I.ringFilterBasis.SubmodulesBasis\\; (n\\mapsto I^n • (\\top : Submodule R M))$$$

Lean4

theorem adic_module_basis : I.ringFilterBasis.SubmodulesBasis fun n : ℕ => I ^ n • (⊤ : Submodule R M) :=
  { inter := fun i j =>
      ⟨max i j,
        le_inf_iff.mpr
          ⟨smul_mono_left <| pow_le_pow_right (le_max_left i j), smul_mono_left <| pow_le_pow_right (le_max_right i j)⟩⟩
    smul := fun m i =>
      ⟨(I ^ i • ⊤ : Ideal R), ⟨i, by simp⟩, fun a a_in =>
        by
        replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
        exact smul_mem_smul a_in mem_top⟩ }

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