isLimitEquivIsTerminalOfIsEmpty — Mathlib

English

If J is empty, a cone over F is limiting iff its cone point is terminal; i.e., IsLimit c ≃ IsTerminal c.pt under IsEmpty J.

Русский

Если J пуст, конус над F является ограничивающим тогда и только тогда, когда точка конуса терминальна; то есть IsLimit c ≃ IsTerminal c.pt при условии IsEmpty J.

LaTeX

$$$[IsEmpty J] \\Rightarrow IsLimit(c) \\simeq IsTerminal(c.pt)$$$

Lean4

/-- If `F` is an empty diagram, then a cone over `F` is limiting iff the cone point is terminal. -/
noncomputable def isLimitEquivIsTerminalOfIsEmpty {J : Type*} [Category J] [IsEmpty J] {F : J ⥤ C} (c : Cone F) :
    IsLimit c ≃ IsTerminal c.pt :=
  (IsLimit.whiskerEquivalenceEquiv (equivalenceOfIsEmpty (Discrete PEmpty.{1}) _)).trans
    (isLimitEmptyConeEquiv _ _ _ (.refl _))

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