Commutative group objects

Stream: Is there code for X?

[Markus Himmel]

I am interested in the following statements:

• If $\mathcal{C}$ is an additive category, then every object of $\mathcal{C}$ can be made into an abelian group object in $\mathcal{C}$ in a canonical way.
• A finite-product-preserving functor between categories with finite products maps abelian group objects to abelian group objects.
• An abelian group object in the category of types is an abelian group.

All of these should be easy to obtain by building CommGrp_ on top of docs#CommMon_. I wonder if someone has already written some relevant code in this direction. Perhaps @Sophie Morel? I am also aware of @Joël Riou's development at #mathlib4 > Definition of group scheme? @ 💬, and there are several other suggestions in that thread, so I'm not sure what the correct thing to put into mathlib would be.

[Joël Riou]

We should also ping @Adam Topaz.

[Sophie Morel]

I was in a workshop where we wrote a definition of group objects last May, but we restricted ourselves to the case of categories with finite products. We proved your second point (for groups, not abelian groups), but not the third.

[Sophie Morel]

The code is there:
https://github.com/leanprover-community/mathlib4/tree/ICMS2024.GroupObject?tab=repositories
but to be honest I haven't touched it since and I'm not sure it's very useful... Sorry I don't have a more satisfying answer.