limitCone — Mathlib

English

The constructed limit cone for F: J ⥤ CommMonCat is a limit cone; i.e., it satisfies the universal property in CommMonCat.

Русский

Сконструированный предел-конус для F: J ⥤ CommMonCat является пределом; т. е. удовлетворяет универсальному свойству предела в CommMonCat.

LaTeX

$$$\text{limitConeIsLimit } F$$$

Lean4

/-- A choice of limit cone for a functor into `CommMonCat`.
(Generally, you'll just want to use `limit F`.)
-/
@[to_additive /-- A choice of limit cone for a functor into `AddCommMonCat`.
    (Generally, you'll just want to use `limit F`.) -/
    ]
noncomputable def limitCone : Cone F :=
  liftLimit (limit.isLimit (F ⋙ forget₂ CommMonCat.{u} MonCat.{u}))

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