hasTerminal_of_unique — Mathlib

English

If there is an object X such that every Y has a unique morphism Y → X (i.e., nonempty and subsingleton Hom-sets Y → X), then C has a terminal object.

Русский

Если существует объект X, который к каждому Y имеет единственную стрелу Y → X, то у C есть терминальный объект.

LaTeX

$$$\\exists X\\in\\mathrm{Obj}(C)\\quad\\text{such that }\\forall Y,\\; |\\mathrm{Hom}(Y,X)|=1 . \\Rightarrow \\mathrm{HasTerminal}(C).$$$

Lean4

/-- We can more explicitly show that a category has a terminal object by specifying the object,
and showing there is a unique morphism to it from any other object. -/
theorem hasTerminal_of_unique (X : C) [∀ Y, Nonempty (Y ⟶ X)] [∀ Y, Subsingleton (Y ⟶ X)] : HasTerminal C where
  has_limit
    F := .mk ⟨_, (isTerminalEquivUnique F X).invFun fun _ ↦ ⟨Classical.inhabited_of_nonempty', (Subsingleton.elim · _)⟩⟩

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