doc-next-gen

Mathlib.Topology.Algebra.Module.Simple

Module docstring

{"# 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. "}

LinearMap.isClosed_or_dense_ker theorem
(l : M →ₗ[R] N) : IsClosed (LinearMap.ker l : Set M) ∨ Dense (LinearMap.ker l : Set M)
Full source 
/-- 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) :
    IsClosedIsClosed (LinearMap.ker l : Set M) ∨ Dense (LinearMap.ker l : Set M) := by
  rcases l.surjective_or_eq_zero with (hl | rfl)
  · exact (LinearMap.ker l).isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
  · rw [LinearMap.ker_zero]
    left
    exact isClosed_univ
Kernel of Linear Map to Simple Module is Closed or Dense
Informal description
Let $M$ and $N$ be modules over a ring $R$, with $N$ being a simple module. For any linear map $l: M \to N$, the kernel $\ker l$ is either closed or dense in $M$ (with respect to the topology on $M$).