instAddCommMonoidElemForallObjCompForgetSections

Mathlib.Algebra.Category.ModuleCat.Limits

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

English

The sections form an AddCommMonoid, inherited from the forgetful functor to AddCommMonoid.

Русский

Секции образуют AddCommMonoid, наследуемый от забывающего функторa в AddCommMonoid.

LaTeX

$$$$ \\text{sections} \\in \\mathrm{AddCommMonoid} $$$$

Lean4

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

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

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

Разделы

Аффилиация

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