uniqueOfEpiZero — Mathlib

English

If the zero morphism from X to M is epi, then M is a singleton (has a unique element).

Русский

Если нулевой морфизм X → M является эпиморфизмом, то M является синглетным множеством (один элемент).

LaTeX

$$$\\forall X\\,\\forall M\\ [Epi(0: X \\to M) \\Rightarrow] Unique\; M$$$

Lean4

/-- If the zero morphism is an epi then the codomain is trivial. -/
def uniqueOfEpiZero (X) [h : Epi (0 : X ⟶ of R M)] : Unique M :=
  uniqueOfSurjectiveZero X ((ModuleCat.epi_iff_surjective _).mp h)

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