English
The topology on M induced by a ModuleFilterBasis on a module over a topological ring is given by the AddGroupFilterBasis topology.
Русский
Топология на модуле M, индуцированная ModuleFilterBasis, задаётся через топологию AddGroupFilterBasis базиса.
LaTeX
$$$\text{topology}'(BM) = BM.toAddGroupFilterBasis.topology$.$$
Lean4
/-- If `R` is discrete then the trivial additive group filter basis on any `R`-module is a
module filter basis. -/
instance [DiscreteTopology R] : Inhabited (ModuleFilterBasis R M) :=
⟨{
show AddGroupFilterBasis M from
default with
smul' := by
rintro U (rfl : U ∈ {{(0 : M)}})
use univ, univ_mem, {0}, rfl
rintro a ⟨x, -, m, rfl, rfl⟩
simp only [smul_zero, mem_singleton_iff]
smul_left' := by
rintro x₀ U (h : U ∈ {{(0 : M)}})
rw [mem_singleton_iff] at h
use {0}, rfl
simp [h]
smul_right' := by
rintro m₀ U (h : U ∈ (0 : Set (Set M)))
rw [Set.mem_zero] at h
simp [h, nhds_discrete] }⟩
