Countable covers by closed submodules

Let A be a ring with a topology in which zero is a limit of units, for instance a nontrivially normed field. A topological module over A has no proper submodule with nonempty interior (Mathlib's Submodule.eq_top_of_nonempty_interior'). In a Baire module, the Baire category theorem then shows that countably many proper closed submodules never cover the whole module. This is the form in which Baire category enters gliding-hump arguments that choose a vector avoiding countably many closed subspaces at once, such as the inductive constructions used for separating ideals of Banach algebras.

Main results

• Submodule.exists_forall_notMem_of_isClosed: a Baire topological module is not the union of countably many proper closed submodules.

theorem Submodule.exists_forall_notMem_of_isClosed {A : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring A] [TopologicalSpace A] [(nhdsWithin 0 {x : A | IsUnit x}).NeBot] [AddCommGroup M] [Module A M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul A M] [BaireSpace M] [Countable ι] (p : ι → Submodule A M) (hc : ∀ (i : ι), IsClosed ↑(p i)) (hp : ∀ (i : ι), p i ≠ ⊤) : ∃ (x : M), ∀ (i : ι), x ∉ p i

A Baire module is not a countable union of proper closed submodules. Over a ring in which zero is a limit of units, some vector of a Baire topological module lies outside each member of a countable family of proper closed submodules.