hasLimit — Mathlib

English

For any small category J and any functor F : J ⥤ CommSemiRingCat, there exists a limit of F in CommSemiRingCat.

Русский

Для любой маленькой категории J и любой функтор F : J ⥤ CommSemiRingCat существует предел F в CommSemiRingCat.

LaTeX

$$$ \\operatorname{HasLimit}(F) $$$

Lean4

/-- If `(F ⋙ forget CommSemiRingCat).sections` is `u`-small, `F` has a limit. -/
instance hasLimit : HasLimit F :=
  ⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} F⟩

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