isZero_of_subsingleton — Mathlib

English

If an R-module M is a subsingleton, then M is a zero object in ModuleCat R.

Русский

Если модуль R-M является подсинглетоном, то он является нулевым объектом в ModuleCat R.

LaTeX

$$$ [\text{Subsingleton } M] \Rightarrow \mathrm{IsZero}(M) $$$

Lean4

theorem isZero_of_subsingleton (M : ModuleCat R) [Subsingleton M] : IsZero M
    where
  unique_to
    X :=
    ⟨⟨⟨ofHom (0 : M →ₗ[R] X)⟩, fun f => by
        ext x
        rw [Subsingleton.elim x (0 : M)]
        simp⟩⟩
  unique_from
    X :=
    ⟨⟨⟨ofHom (0 : X →ₗ[R] M)⟩, fun f => by
        ext x
        subsingleton⟩⟩

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