English
A chosen limit cone for a functor into CommRingCat is constructed by transporting a limit cone from RingCat via forgetful functors.
Русский
Выбранный предел-конус для диаграммы в CommRingCat строится перенесением предела из RingCat через функторы забывания.
LaTeX
$$$\text{limitCone } F := \text{liftLimit}(\text{limit.isLimit}(F \circ \mathrm{forget}_2\ CommRingCat))$$$
Lean4
/-- A choice of limit cone for a functor into `CommRingCat`.
(Generally, you'll just want to use `limit F`.)
-/
def limitCone : Cone F :=
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
liftLimit (limit.isLimit (F ⋙ forget₂ CommRingCat.{u} RingCat.{u}))
