forget₂_reflectsLimitsOfSize — Mathlib

English

Let forget₂ be the forgetful functor from ModuleCat(R) to AddCommGrpCat. It reflects limits of size v: limits in ModuleCat can be detected after forgetting to AddComGrp.

Русский

Пусть forget₂: ModuleCat(R) → AddCommGrpCat. Он отражает пределы размерности v: пределы в Mod_R распознаются после отказа до AddCommGrp.

LaTeX

$$$\operatorname{ReflectsLimitsOfSize}_{v,v}(\mathrm{forget}_2(\mathrm{ModuleCat}(R), \mathrm{AddCommGrpCat}))$$$

Lean4

instance forget₂_reflectsLimitsOfSize :
    ReflectsLimitsOfSize.{v, v} (forget₂ (ModuleCat.{max v w} R) AddCommGrpCat.{max v w}) :=
  reflectsLimits_of_reflectsIsomorphisms

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