isTerminalEquivUnique — Mathlib

English

There is a canonical equivalence between Y being terminal in C and the property that for every X in C there exists a unique morphism X→Y.

Русский

Существует каноническое эквивалентность между тем, что Y является терминальным объектом в C, и тем, что для каждого объекта X в C существует единственный морфизм X→Y.

LaTeX

$$$\\text{IsLimit}\\big(\\langle Y,\\ldots\\rangle\\big) \\;\\simeq\\; \\forall X:\\; C,\\; \\text{Unique}(X\\to Y)$$$

Lean4

/-- An object `Y` is terminal iff for every `X` there is a unique morphism `X ⟶ Y`. -/
def isTerminalEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (Y : C) :
    IsLimit (⟨Y, by cat_disch, by simp⟩ : Cone F) ≃ ∀ X : C, Unique (X ⟶ Y)
    where
  toFun t
    X :=
    { default := t.lift ⟨X, ⟨by cat_disch, by simp⟩⟩
      uniq := fun f => t.uniq ⟨X, ⟨by cat_disch, by simp⟩⟩ f (by simp) }
  invFun
    u :=
    { lift := fun s => (u s.pt).default
      uniq := fun s _ _ => (u s.pt).2 _ }
  left_inv := by dsimp [Function.LeftInverse]; intro x; simp only [eq_iff_true_of_subsingleton]
  right_inv := by
    dsimp [Function.RightInverse, Function.LeftInverse]
    subsingleton

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