isTerminalIffObj — Mathlib

English

An equivalence between IsTerminal X and IsTerminal (G.obj X) when G preserves and reflects the empty diagram limit.

Русский

Эквивалентность между IsTerminal X и IsTerminal(G.obj X) при сохранении и отражении пустого диаграммного предела.

LaTeX

$$$\\text{isTerminalIffObj}(G,X) : \\operatorname{IsTerminal} X \\simeq \\operatorname{IsTerminal}(G(X)).$$$

Lean4

/-- A functor that preserves and reflects terminal objects induces an equivalence on
`IsTerminal`. -/
def isTerminalIffObj [PreservesLimit (Functor.empty.{0} C) G] [ReflectsLimit (Functor.empty.{0} C) G] (X : C) :
    IsTerminal X ≃ IsTerminal (G.obj X)
    where
  toFun := IsTerminal.isTerminalObj G X
  invFun := IsTerminal.isTerminalOfObj G X
  left_inv := by cat_disch
  right_inv := by cat_disch

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