English
Under suitable topological linearity assumptions and the existence of enough units near zero, a submodule with nonempty interior must be the whole space.
Русский
При наличии достаточного числа единиц near нуля и подмодуль с непустым interior обязан быть всем пространством.
LaTeX
$$$\\text{if interior nonempty then } s=\\top$$$
Lean4
/-- If `M` is a topological module over `R` and `0` is a limit of invertible elements of `R`, then
`⊤` is the only submodule of `M` with a nonempty interior.
This is the case, e.g., if `R` is a nontrivially normed field. -/
theorem eq_top_of_nonempty_interior' [NeBot (𝓝[{x : R | IsUnit x}] 0)] (s : Submodule R M)
(hs : (interior (s : Set M)).Nonempty) : s = ⊤ :=
by
rcases hs with ⟨y, hy⟩
refine Submodule.eq_top_iff'.2 fun x => ?_
rw [mem_interior_iff_mem_nhds] at hy
have : Tendsto (fun c : R => y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 (y + (0 : R) • x)) :=
tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).smul tendsto_const_nhds)
rw [zero_smul, add_zero] at this
obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ := nonempty_of_mem (inter_mem (Filter.mem_map.1 (this hy)) self_mem_nhdsWithin)
have hy' : y ∈ ↑s := mem_of_mem_nhds hy
rwa [s.add_mem_iff_right hy', ← Units.smul_def, s.smul_mem_iff' u] at hu
