limitCone — Mathlib

English

The chosen cone is a limit cone for the diagram F; i.e., it has the universal property of a limit.

Русский

Выбранный конус является пределом диаграммы F, то есть обладает универсальным свойством предела.

LaTeX

$$$ \\operatorname{IsLimit}( \\text{limitCone } F )$$$

Lean4

/-- A choice of limit cone for a functor into `RingCat`.
(Generally, you'll just want to use `limit F`.)
-/
def limitCone : Cone F :=
  let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  liftLimit (limit.isLimit (F ⋙ forget₂ RingCat.{u} SemiRingCat.{u}))

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