Abbreviations when naming categories

Stream: mathlib4

[Michał Mrugała]

There is a discussion about what the category of commutative algebras should be called (#23601), and by extensions how should we name similar categories. There are three versions proposed:

1. CommAlg, if we use this convention we should probably rename AlgebraCat to Alg. This agrees with the notation for Grp and CommGrp. It also is analogous to how <algebraic object>-object categories are named: Mon_ C, Grp_ C etc.
2. CommAlgCat, agrees with category names such as MonCat and RingCat. It also makes clear that we're talking about a category, and hopefully allows us to avoid issues with overzealous abbreviation (see docs#Doset.doset).
3. CommAlgebraCat, agrees withAlgebraCat. This option is arguably the most consistent with the current naming in mathlib, but it is a mouthful.

I think the first convention is the best as long as it doesn't cause any issues, and we might want to consider renaming other categories to have consistent notation across the board.

[Bhavik Mehta]

I'm in favour of the second or third: names like Alg in the global namespace are ambiguous and confusing for not much good reason; see also the discussion here #mathlib4 > Naming convention @ 💬. The only examples we have of that style are Grp and CommGrp, which in my eyes are unfortunate exceptions to the otherwise sensible convention that exists.

With version 1, it's also not clear what happens to something like RingCat: I don't like the idea of naming some of them -Cat and some of them not, depending on the naming choices used elsewhere in mathlib! This is a really easy way to make the naming convention hard to predict

[Michał Mrugała]

I guess we could change RingCat to Rng, but I can see that getting hairy

[Yaël Dillies]

There's a fourth option which is to put those definitions in a namespace. Personally, I find it a bit odd that docs#Mon_ is in the root namespace when category theory is otherwise very consistently namespaced

[Bhavik Mehta]

Yeah, if these are in a namespace then I'm happy with Grp and Ring and Alg to be the names

[Kevin Buzzard]

Do you really mean Ring? With open CategoryTheory I should imagine that this would cause trouble. Or do you mean Rng?

[Edward van de Meent]

I imagine calling it Rng might give at least some confusion to new users, since this sometimes refers to a ring without identity element (since you drop the "i")