hasLimit — Mathlib

English

If the shape J is small (in the appropriate universe), the functor F: J ⥤ MonCat has a limit in MonCat.

Русский

Если форма J является маленькой (в соответствующей вселенной), то диаграмма F: J ⥤ MonCat имеет предел в MonCat.

LaTeX

$$$\text{HasLimit } F \;\text{provided }[\text{Small}.{u} (\text{Functor.sections}(F \downarrow \text{forget MonCat}))]$$$

Lean4

/-- If `(F ⋙ forget MonCat).sections` is `u`-small, `F` has a limit. -/
@[to_additive /-- If `(F ⋙ forget AddMonCat).sections` is `u`-small, `F` has a limit. -/
    ]
instance hasLimit : HasLimit F :=
  HasLimit.mk
    { cone := limitCone F
      isLimit := limitConeIsLimit F }

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