English
The chosen limit cone for a functor into CommGrpCat is indeed a limit cone; i.e., it satisfies the universal property of a limit.
Русский
Выбор предельного конуса для диаграммы в CommGrpCat действительно является пределом; обладает универсальной свойством предела.
LaTeX
$$$ \text{limitConeIsLimit } F : IsLimit(\text{limitCone } F)$$$
Lean4
/-- A choice of limit cone for a functor into `CommGrpCat`.
(Generally, you'll just want to use `limit F`.) -/
@[to_additive /-- A choice of limit cone for a functor into `AddCommGrpCat`.
(Generally, you'll just want to use `limit F`.) -/
]
noncomputable def limitCone : Cone F :=
letI : Small.{u} (Functor.sections ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat)) :=
inferInstanceAs <| Small (Functor.sections (F ⋙ forget CommGrpCat))
liftLimit (limit.isLimit (F ⋙ forget₂ CommGrpCat.{u} GrpCat.{u}))
