feat: port Topology.Algebra.Module.Simple (#3307)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -1625,6 +1625,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Ring
 import Mathlib.Topology.Algebra.Localization
 import Mathlib.Topology.Algebra.Module.Basic
 import Mathlib.Topology.Algebra.Module.LinearPMap
+import Mathlib.Topology.Algebra.Module.Simple
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Algebra.Nonarchimedean.Basic

Mathlib/Topology/Algebra/Module/Simple.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+
+! This file was ported from Lean 3 source module topology.algebra.module.simple
+! leanprover-community/mathlib commit f430769b562e0cedef59ee1ed968d67e0e0c86ba
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.RingTheory.SimpleModule
+import Mathlib.Topology.Algebra.Module.Basic
+
+/-!
+# The kernel of a linear function is closed or dense
+
+In this file we prove (`LinearMap.isClosed_or_dense_ker`) that the kernel of a linear function
+`f : M →ₗ[R] N` is either closed or dense in `M` provided that `N` is a simple module over `R`. This
+applies, e.g., to the case when `R = N` is a division ring.
+-/
+
+
+universe u v w
+
+variable {R : Type u} {M : Type v} {N : Type w} [Ring R] [TopologicalSpace R] [TopologicalSpace M]
+  [AddCommGroup M] [AddCommGroup N] [Module R M] [ContinuousSMul R M] [Module R N] [ContinuousAdd M]
+  [IsSimpleModule R N]
+
+set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
+/-- The kernel of a linear map taking values in a simple module over the base ring is closed or
+dense. Applies, e.g., to the case when `R = N` is a division ring. -/
+theorem LinearMap.isClosed_or_dense_ker (l : M →ₗ[R] N) :
+    IsClosed (LinearMap.ker l : Set M) ∨ Dense (LinearMap.ker l : Set M) := by
+  rcases l.surjective_or_eq_zero with (hl | rfl)
+  · exact l.ker.isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
+  · rw [LinearMap.ker_zero]
+    left
+    exact isClosed_univ
+#align linear_map.is_closed_or_dense_ker LinearMap.isClosed_or_dense_ker