instPreservesLimitTopCatForget₂OfHasLimitOfModuleCatCompForget

English

There is a limit structure on TopModuleCat that is compatible with the forgetful functor to ModuleCat.

Русский

Существуют пределы в TopModuleCat, совместимые с забывающим функтором в ModuleCat.

LaTeX

$$$\\text{instHasLimitsOfShapeOfModuleCat}$$$

Lean4

instance {J : Type*} [Category J] {F : J ⥤ TopModuleCat.{v} R} [HasLimit (F ⋙ forget₂ _ (ModuleCat.{v} R))]
    [PreservesLimit (F ⋙ forget₂ _ (ModuleCat.{v} R)) (forget _)] : PreservesLimit F (forget₂ _ TopCat) :=
  preservesLimit_of_preserves_limit_cone (isLimit (limit.isLimit _))
    (TopCat.isLimitConeOfForget (F := F ⋙ forget₂ _ TopCat)
      ((forget _).mapCone (getLimitCone (F ⋙ forget₂ _ (ModuleCat.{v} R))).1 :)
      (isLimitOfPreserves (forget (ModuleCat R)) (limit.isLimit _)))

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