subsingleton_iff_ker_eq_top — Mathlib

English

For a localized map g, Subsingleton M' is equivalent to ker g = ⊤, i.e., the entire domain collapses under g.

Русский

Для локализованного отображения g, выполняется равенство Subsingleton M' ⇔ ker g = ⊤, то есть вся область определения сжата под g.

LaTeX

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

Lean4

theorem subsingleton_iff_ker_eq_top {S : Submonoid R} :
    Subsingleton (LocalizedModule S M) ↔ LinearMap.ker (LocalizedModule.mkLinearMap S M) = ⊤ :=
  IsLocalizedModule.subsingleton_iff_ker_eq_top S _

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