limitCone — Mathlib

English

If the underlying section of F is small, then F has a limit in CommSemiRingCat.

Русский

Если секции F по меньшему размеру, то F имеет предел в CommSemiRingCat.

LaTeX

$$$\operatorname{HasLimit}\,F$$$

Lean4

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

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