subsingleton_iff_ker_eq_top — Mathlib

English

For a localized linear map g, the target module M' is a singleton if and only if the kernel of g is the whole source module M (i.e., ker g = ⊤).

Русский

Для локализованного линейного отображения g целевой модуль M' является одноэлементным тогда и только тогда, когда ядро g равно всему источному модулю M (ker g = ⊤).

LaTeX

$$$\operatorname{Subsingleton}(M') \iff \ker g = \top$$$

Lean4

theorem subsingleton_iff_ker_eq_top (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] :
    Subsingleton M' ↔ LinearMap.ker g = ⊤ := by
  rw [← top_le_iff]
  refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x
  simpa using @H x Submodule.mem_top

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