instModuleElemForallObjCompForgetSections

Mathlib.Algebra.Category.ModuleCat.Limits

URI: https://scilib.ai/kg/mathlib#ModuleCat.instModuleElemForallObjCompForgetSections

English

There is an AddCommMonoid structure on the sections object induced by forgetting to AddCommGrp.

Русский

Объект секций наделяется структурой AddCommMonoid через забывание до AddCommGrp.

LaTeX

$$$$ \\text{ModulesCat.sectionsSubmodule}(F) \\text{ carries an } \\mathrm{AddCommMonoid} $$$$

Lean4

instance : Module R (F ⋙ forget (ModuleCat R)).sections :=
  inferInstanceAs <| Module R (sectionsSubmodule F)

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

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

Разделы

Аффилиация

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