English
The limit cone vertex in CommMonCat carries a CommMonoid structure, i.e., the limit of a diagram F: J ⥤ CommMonCat is computed level-wise as a commutative monoid.
Русский
У вершины предела в CommMonCat есть структура CommMonoid; предел диаграммы F: J ⥤ CommMonCat вычисляется поэлементно как коммутативный моноид.
LaTeX
$${ $\text{limitCommMonoid } F$ is a CommMonoid on the vertex of the limit cone }$$
Lean4
@[to_additive]
noncomputable instance limitCommMonoid : CommMonoid (Types.Small.limitCone (F ⋙ forget CommMonCat.{u})).pt :=
letI : CommMonoid (F ⋙ forget CommMonCat.{u}).sections :=
@Submonoid.toCommMonoid (∀ j, F.obj j) _ (MonCat.sectionsSubmonoid (F ⋙ forget₂ CommMonCat.{u} MonCat.{u}))
inferInstanceAs <| CommMonoid (Shrink (F ⋙ forget CommMonCat.{u}).sections)
