English
The limit of a diagram in CommGrpCat is a commutative group, with the limit cone inherited from the underlying GrpCat limit.
Русский
Предел диаграммы в CommGrpCat является коммутативной группой; пределовый конус наследуется от соответствующего предела в GrpCat.
LaTeX
$$$ \text{CommGrpCat.limitCommGroup } F \text{ is a CommGroup with the limit cone induced by the GrpCat limit}$$$
Lean4
@[to_additive]
noncomputable instance limitCommGroup [Small.{u} (Functor.sections (F ⋙ forget CommGrpCat))] :
CommGroup (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat.{u})).pt :=
letI : CommGroup (F ⋙ forget CommGrpCat.{u}).sections :=
@Subgroup.toCommGroup (∀ j, F.obj j) _ (GrpCat.sectionsSubgroup (F ⋙ forget₂ CommGrpCat.{u} GrpCat.{u}))
inferInstanceAs <| CommGroup (Shrink (F ⋙ forget CommGrpCat.{u}).sections)
