[Merged by Bors] - feat(CategoryTheory): group objects

[TwoFX]

Define group objects in cartesian monoidal categories.

Show that the associativity diagram of a group object is always cartesian and deduce that morphisms of group objects commute with taking inverses.

Show that a finite-product-preserving functor takes group objects to group objects.

---

• depends on: [Merged by Bors] - feat(CategoryTheory): more API for ChosenFiniteProducts #21509

[github-actions]

PR summary d575b258af

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ (new file)	591
Mathlib.CategoryTheory.Monoidal.Grp_ (new file)	617

---

Declarations diff

+ Grp_
+ comp'
+ comp_hom
+ eq_lift_inv_left
+ eq_lift_inv_right
+ forget
+ forget₂Mon_
+ forget₂Mon_comp_forget
+ forget₂Mon_map_hom
+ forget₂Mon_obj_mul
+ forget₂Mon_obj_one
+ fullyFaithfulForget₂Mon_
+ hom_ext
+ id'
+ id_hom
+ instance : (forget C).Faithful
+ instance : (forget₂Mon_ C).Faithful := InducedCategory.faithful _
+ instance : (forget₂Mon_ C).Full := InducedCategory.full _
+ instance : Category (Grp_ C)
+ instance : HasInitial (Grp_ C)
+ instance : Inhabited (Grp_ C)
+ inv_hom
+ isPullback
+ lift_comp_inv_left
+ lift_comp_inv_right
+ lift_comp_one_left
+ lift_comp_one_right
+ lift_inv_comp_left
+ lift_inv_comp_right
+ lift_inv_left_eq
+ lift_inv_right_eq
+ lift_lift_assoc
+ mapGrp
+ mapGrpFunctor
+ mkIso
+ mkIso_hom_hom
+ mkIso_inv_hom
+ trivial
+ uniqueHomFromTrivial

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[erdOne]

LGTM and I would want this in mathlib very much but I don't think I am familiar enough with the monoidal category library to maintainer merge this.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): more API for ChosenFiniteProducts #21509
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

Thanks for the work! I didn't know you were working on this, and was planning to work with PKU students to define group schemes as group objects in the category over a base scheme (with the cartesian monoidal structure). It seems mathlib doesn't have the Monoid instance on X ⟶ M if M is a monoid object (with cartesian product) and X is arbitrary. Do you also have group schemes in mind and do you plan to do anything about that? You did touch the cartesian file, but aren't adding much.

For elliptic curves we might need "MulAction objects" which are actually two objects M and S in a category equipped with a morphism M × S ⟶ S satisfying axioms, where M is a monoid/group object. I'm wondering whether we can use some automation to get the MulAction of X ⟶ M on X ⟶ S; I don't know whether the work of @adamtopaz on Lawvere theory is relevant here.

The next goal would be the anti-equivalence between the category of affine group schemes to HopfAlgebraCat, as Hopf algebras can be seen as cogroup objects (w.r.t. coproduct, i.e. tensor product) in the category of R-algebras. (On the other hand R-algebras can be seen as monoid objects in R-Mod w.r.t. tensor product, which is super confusing ...)

[erdOne]

It seems mathlib doesn't have the Monoid instance on X ⟶ M if M is a monoid object (with cartesian product) and X is arbitrary

#21394

[alreadydone]

It seems mathlib doesn't have the Monoid instance on X ⟶ M if M is a monoid object (with cartesian product) and X is arbitrary.

Maybe the plan is to do this via #21576; if X M : C then (X ⟶ ·) is a monoidal functor from C to Type*, and so if M is a monoid/group object then X ⟶ M is also a monoid/group object, and a monoid/group object in Type* has a Monoid/Group instance on it.
@erdOne Can you comment whether/how #21394 is connected to this?

[erdOne]

Sorry, should have given a more precise link
Is this not what you are talking about?

[alreadydone]

Thanks! I should have spotted it. I'm surprised Mon_ C isn't just defined to be X : C + Mon_Class X.

[TwoFX]

I'm surprised Mon_ C isn't just defined to be X : C + Mon_Class X.

I think the reason for this is simply that Mon_ is much older than Mon_Class and no one has done the refactor yet.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style