forget_reflectsLimits — Mathlib

English

The forgetful functor forget from Mod_R to Type reflects limits (i.e., detects when a cone is a limit cone).

Русский

Забывающий функтор forget из Mod_R в Type отражает пределы (распознаёт, когда конус является пределом).

LaTeX

$$$\operatorname{ReflectsLimits}(\mathrm{forget}(\mathrm{Mod}_R))$$$

Lean4

instance forget_reflectsLimits : ReflectsLimits (forget (ModuleCat.{v} R)) :=
  ModuleCat.forget_reflectsLimitsOfSize.{v, v}

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