commGroupObj — Mathlib

English

For each object j in a diagram F : J ⥤ CommGrpCat, the object F(j) inherits a commutative group structure.

Русский

Для каждого объекта j диаграммы F : J ⥤ CommGrpCat объект F(j) имеет структуру коммутативной группы.

LaTeX

$$$ \forall j,\; F(j) \text{ has a } \mathrm{CommGroup} \text{ structure}$$$

Lean4

@[to_additive]
instance commGroupObj (j) : CommGroup ((F ⋙ forget CommGrpCat).obj j) :=
  inferInstanceAs <| CommGroup (F.obj j)

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