instCreatesLimitsOfShapeModuleCatForget₂

English

There is a canonical construction showing that forget₂ creates limits of shape J.

Русский

Существует каноническое построение, доказывающее, что forget₂ создаёт пределы формы J.

LaTeX

$$$\operatorname{CreatesLimitsOfShape}(J,\ \operatorname{forget}_2( FGModuleCat(k), ModuleCat(k) ))$$$

Lean4

instance : CreatesLimitsOfShape J (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) where
  CreatesLimit {F} := forget₂CreatesLimit F

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