hasInitial_of_unique — Mathlib

English

If there exists an X with unique arrows X → Y to every Y, then HasInitial C.

Русский

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

LaTeX

$$$\\forall X,\\; (\\forall Y, \\mathrm{Hom}(X,Y) \\text{ is singleton}) \\Rightarrow \\mathrm{HasInitial}(C).$$$

Lean4

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

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