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.
theorem
LinearMap.isClosed_or_dense_ker
{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]
(l : M →ₗ[R] N)
:
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.