isClosed_or_dense_ker — Mathlib

English

For a linear map l: M → N with N simple over R, ker(l) is either closed or dense in M.

Русский

Для линейного отображения l: M → N с простым модулем N над R, ядро l либо замкнуто, либо плотное в M.

LaTeX

$$$\ker(l) \;\text{is either closed or dense in } M.$$$

Lean4

/-- 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 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 (LinearMap.ker l).isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
  · rw [LinearMap.ker_zero]
    left
    exact isClosed_univ

Похожие утверждения