terminalIffUnique — Mathlib

English

There is an equivalence IsTerminal X ≃ Unique (ToType X) for a concrete category modulo preservation of terminal objects by forgetful functor.

Русский

Существует эквивалентность IsTerminal X ≃ Unique (ToType X) для конкретной категории с сохранением терминала забывающей функторы.

LaTeX

$$$ IsTerminal X \\simeq Unique (ToType X) $$$

Lean4

/-- The equivalence `IsTerminal X ≃ Unique (ToType X)` if the forgetful functor
preserves and reflects terminals. -/
noncomputable def terminalIffUnique [PreservesLimit (Functor.empty.{0} C) (forget C)]
    [ReflectsLimit (Functor.empty.{0} C) (forget C)] (X : C) : IsTerminal X ≃ Unique (ToType X) :=
  (IsTerminal.isTerminalIffObj (forget C) X).trans <| Types.isTerminalEquivUnique _

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