feat(topology/algebra/module/basic): a hyperplane is either closed or…

… dense (#16782)

src/topology/algebra/module/basic.lean

@@ -12,6 +12,7 @@ import algebra.algebra.basic
 import linear_algebra.projection
 import linear_algebra.pi
 import linear_algebra.determinant
+import ring_theory.simple_module
 
 /-!
 # Theory of topological modules and continuous linear maps.
@@ -167,10 +168,13 @@ S.to_add_subgroup.topological_add_group
 end submodule
 
 section closure
-variables {R : Type u} {M : Type v}
+variables {R R' : Type u} {M M' : Type v}
 [semiring R] [topological_space R]
+[ring R'] [topological_space R']
 [topological_space M] [add_comm_monoid M]
+[topological_space M'] [add_comm_group M']
 [module R M] [has_continuous_smul R M]
+[module R' M'] [has_continuous_smul R' M']
 
 lemma submodule.closure_smul_self_subset (s : submodule R M) :
   (λ p : R × M, p.1 • p.2) '' (set.univ ×ˢ closure s) ⊆ closure s :=
@@ -238,6 +242,24 @@ instance {M' : Type*} [add_comm_monoid M'] [module R M'] [uniform_space M']
   complete_space U.topological_closure :=
 is_closed_closure.complete_space_coe
 
+/-- A maximal proper subspace of a topological module (i.e a `submodule` satisfying `is_coatom`)
+is either closed or dense. -/
+lemma submodule.is_closed_or_dense_of_is_coatom (s : submodule R M) (hs : is_coatom s) :
+  is_closed (s : set M) ∨ dense (s : set M) :=
+(hs.le_iff.mp s.submodule_topological_closure).swap.imp (is_closed_of_closure_subset ∘ eq.le)
+  submodule.dense_iff_topological_closure_eq_top.mpr
+
+lemma linear_map.is_closed_or_dense_ker [has_continuous_add M'] [is_simple_module R' R']
+  (l : M' →ₗ[R'] R') :
+  is_closed (l.ker : set M') ∨ dense (l.ker : set M') :=
+begin
+  rcases l.surjective_or_eq_zero with (hl|rfl),
+  { refine l.ker.is_closed_or_dense_of_is_coatom (linear_map.is_coatom_ker_of_surjective hl) },
+  { rw linear_map.ker_zero,
+    left,
+    exact is_closed_univ },
+end
+
 end closure
 
 /-- Continuous linear maps between modules. We only put the type classes that are necessary for the

src/topology/algebra/module/finite_dimension.lean

@@ -197,6 +197,19 @@ lemma linear_map.continuous_iff_is_closed_ker (l : E →ₗ[𝕜] 𝕜) :
   continuous l ↔ is_closed (l.ker : set E) :=
 ⟨λ h, is_closed_singleton.preimage h, l.continuous_of_is_closed_ker⟩
 
+/-- Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is
+    automatically continuous. -/
+lemma linear_map.continuous_of_nonzero_on_open (l : E →ₗ[𝕜] 𝕜) (s : set E) (hs₁ : is_open s)
+  (hs₂ : s.nonempty) (hs₃ : ∀ x ∈ s, l x ≠ 0) : continuous l :=
+begin
+  refine l.continuous_of_is_closed_ker (l.is_closed_or_dense_ker.resolve_right $ λ hl, _),
+  rcases hs₂ with ⟨x, hx⟩,
+  have : x ∈ interior (l.ker : set E)ᶜ,
+  { rw mem_interior_iff_mem_nhds,
+    exact mem_of_superset (hs₁.mem_nhds hx) hs₃ },
+  rwa hl.interior_compl at this
+end
+
 variables [complete_space 𝕜]
 
 /-- This version imposes `ι` and `E` to live in the same universe, so you should instead use