forget₂AddCommGroup_reflectsLimitOfShape

Mathlib.Algebra.Category.ModuleCat.Limits

URI: https://scilib.ai/kg/mathlib#ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape

English

For any shape J, forget₂ from ModuleCat to AddCommGrpCat reflects limits of shape J.

Русский

Для любой формы формы J забывающий от ModuleCat к AddCommGrpCat отражает предел формы J.

LaTeX

$$$\\text{forget₂AddCommGroup_reflectsLimitOfShape}$$$

Lean4

instance forget₂AddCommGroup_reflectsLimitOfShape : ReflectsLimitsOfShape J (forget₂ (ModuleCat.{w} R) AddCommGrpCat)
    where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru