adicModuleTopology — Mathlib

English

The topology on an R-module M associated to an ideal I is defined by using the module basis built from I^n M.

Русский

Топология на модуле R M, связанная с идеалом I, определяется через базис модуля, образованный I^n M.

LaTeX

$$$\\text{adicModuleTopology} : TopologicalSpace\\; M$$$

Lean4

/-- The topology on an `R`-module `M` associated to an ideal `M`. Submodules $I^n M$,
written `I^n • ⊤` form a basis of neighborhoods of zero. -/
def adicModuleTopology : TopologicalSpace M :=
  @ModuleFilterBasis.topology R M _ I.adic_basis.topology _ _
    (I.ringFilterBasis.moduleFilterBasis (I.adic_module_basis M))

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