Removing underscores from docs#Mon_, docs#Grp_ ...

Stream: mathlib4

[Yaël Dillies]

I would like to discuss a rename @Andrew Yang and I have been thinking about for a while: We would like to get rid of the underscores in docs#Mon_, docs#Grp_, docs#Mod_, docs#Mon_Class, docs#Grp_Class, docs#Mod_Class, etc...

[Yaël Dillies]

These underscores do not follow the naming convention and make for very confusing names when combined with other things. For example docs#CategoryTheory.Monad.instMon_ClassFunctor, among many others.

[Yaël Dillies]

Our suggestion is as follows:

1. Rename docs#Grp to GrpCat. I am painfully aware I performed the opposite rename two years ago.
2. Rename Mon_/Grp_/Mon_Class/Grp_Class/Mod_Class to Mon/Grp/Mod/MonClass/GrpClass/ModClass OR to Mon/Grp/Mod/MonObj/GrpObj/ModObj.
   In either case, we'll need to move to the category theory namespace as docs#Mod is taken. This renamespacing seems like a good thing to me regardless.

[Joël Riou]

This seems ok to me. ( Grp would be the category of group objects and GrpCat would be the category of groups, right?)

[Andrew Yang]

Yes. To be precise, CategoryTheory.Grp for (the category of) group objects and _root_.GrpCat for the category of groups.

[Kim Morrison]

Sure. :-)

[Yaël Dillies]

First PR for Mon_Class and CommMon_Class: #28406

[Bhavik Mehta]

I think this is a good change, and on your point 2 I prefer MonClass over MonObj