instHasLimitsOfShapeOfFinCategory

English

The carrier of the limit of a functor F remains a finite FGModule when viewed via ModuleCat.

Русский

Носитель предела для F остаётся конечным FG-модулем, когда рассматривается как ModuleCat.

LaTeX

$$$\operatorname{ModuleCat.isFG}(k, \operatorname{limit}(F\circ \forget_2(FGModuleCat(k), ModuleCat(k))).carrier)$$$

Lean4

instance (J : Type) [Category J] [FinCategory J] : HasLimitsOfShape J (FGModuleCat.{v} k) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (forget₂ (FGModuleCat k) (ModuleCat.{v} k))

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