English
Let F : J ⥤ RingCat be a diagram. If the underlying diagram obtained by forgetting the RingCat structure has a small set of sections, then F has a limit in RingCat.
Русский
Пусть F : J ⥤ RingCat — диаграмма. Если соответствующая диаграмма без кольцевой структуры имеет малую множество секций, тогда диаграмма F обладает пределом в RingCat.
LaTeX
$$$\operatorname{Small}\big(\mathrm{Sections}(F \circ \operatorname{forget}\text{ RingCat})\big) \Rightarrow \operatorname{HasLimit}(F)$$$
Lean4
/-- If `(F ⋙ forget RingCat).sections` is `u`-small, `F` has a limit. -/
instance hasLimit : HasLimit F :=
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
hasLimit_of_created F (forget₂ RingCat.{u} SemiRingCat.{u})
