forget₂Module_preservesLimits — Mathlib

English

The forgetful functor forget₂: AlgCat(R) → ModuleCat(R) preserves all limits of size UnivLE.

Русский

Забывающий функтор forget₂ AlgCat(R) → ModuleCat(R) сохраняет все пределы заданного размера UnivLE.

LaTeX

$$$$\text{PreservesLimitsOfSize}(\text{forget₂}(\text{AlgCat}(R), \text{ModuleCat}(R))).$$$$

Lean4

instance forget₂Module_preservesLimits : PreservesLimits (forget₂ (AlgCat R) (ModuleCat.{w} R)) :=
  AlgCat.forget₂Module_preservesLimitsOfSize.{w, w}

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