English
An object X is initial iff for every Y there is a unique morphism X ⟶ Y.
Русский
Объект X начален тогда и только тогда, когда для каждого Y существует единственный морфизм X ⟶ Y.
LaTeX
$$$\text{IsInitial}(X) \iff (\forall Y, \mathrm{Unique}(X \to Y))$$$
Lean4
/-- An object `X` is initial iff for every `Y` there is a unique morphism `X ⟶ Y`. -/
def isInitialEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) :
IsColimit (⟨X, ⟨by cat_disch, by simp⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y)
where
toFun t
X :=
{ default := t.desc ⟨X, ⟨by cat_disch, by simp⟩⟩
uniq := fun f => t.uniq ⟨X, ⟨by cat_disch, by simp⟩⟩ f (by simp) }
invFun
u :=
{ desc := fun s => (u s.pt).default
uniq := fun s _ _ => (u s.pt).2 _ }
left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
right_inv :=
by
#adaptation_note /-- 19-07-2025 grind stopped working -/
intro x; dsimp
