forget_reflectsLimitsOfSize — Mathlib

English

Let forgetful functor forget from the category of R-modules to the category of types. The forgetful functor reflects limits of size v: if a cone is a limit cone after forgetting to sets, then it was a limit cone in the category of R-modules.

Русский

Пусть забывающий функтор forget: Mod_R → TypeReflects limits of size v: если конус является пределом после забывания до множеств, то он был пределом и влей в категории модулей.

LaTeX

$$$\operatorname{ReflectsLimitsOfSize}_{v,v}(\mathrm{forget}(\mathrm{Mod}_R))$$$

Lean4

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

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