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")

[Andrew Yang]

I am still not sure how you will solve the Ring issue.

[Yaël Dillies]

This one can stay RingCat for the time being. I don't think that's an issue

[Andrew Yang]

Are people okay with this? I don't think people will be happy with such inconsistencies when the whole conversation stemmed from an inconsistency introduced in #23601

[Yaël Dillies]

There was no inconsistency in the first place since CommAlgebra isn't a typeclass that exists

[Andrew Yang]

The original naming convention was to append Cat for every concrete category regardless if it is one single typeclass or a conjunction of several. See docs#FGModuleCat or docs#TopCommRingCat

[Yaël Dillies]

Order theoretic categories were intended not to follow this convention from the start, eg docs#Lat

[Eric Wieser]

Andrew Yang said:

I am still not sure how you will solve the Ring issue.

Does protected structure CategoryTheory.Ring work? (and making users write open CategoryTheory (Ring))

[Yaël Dillies]

The issue with your Cat convention (which btw came about amidst the port, without much discussion) is that it creates lengthy names which keep on appearing in more and more definitions.

[Yaël Dillies]

As a result, we are witnessing a second order naming convention of removing the Cat suffix in definition names, eg docs#BialgebraCat.hasForgetToAlgebra.

[Andrew Yang]

Yaël Dillies said:

As a result, we are witnessing a second order naming convention of removing the Cat suffix in definition names, eg docs#BialgebraCat.hasForgetToAlgebra.

That name is just plain wrong.

[Yaël Dillies]

It seems much better to me to fix the names straight up

[Yaël Dillies]

Andrew Yang said:

That name is just plain wrong.

It's a natural consequence of the suffixing Cat convention

[Andrew Yang]

How it is natural when you look at #naming and go through the bullet points one by one and you would never end up with a name like that?

[Andrew Yang]

Here's a nonsense (but at least consistent) option: We call them by their short usual name (without Cat) so that we can justify short names in lemmas, namespace and protect them, but add scoped notation 𝐑𝐢𝐧𝐠 := CategoryTheory.Ring since this is what we write on paper as well.

[Yaël Dillies]

That would be fine by me. All I want is not having to type VeryLongNameCat

[Eric Wieser]

What's wrong with protected as I suggest above, instead of tricky unicode?

[Andrew Yang]

Because I don't want to write CategoryTheory.CommRing everywhere?

[Andrew Yang]

(which is longer than the current one which Yael wants to shorten)

[Eric Wieser]

Eric Wieser said:

and making users write open CategoryTheory (Ring)

[Andrew Yang]

But I need my old CommRings as well.

[Eric Wieser]

Is that actually the case after you've set up the basic of the category?

[Andrew Yang]

We often need to translate non-category theoretic results into category theory in proofs as well. I don't think it is avoidable unless you copy the whole RingTheory folder and make a category version. I might not need to actually write [CommRing R] but they will still both appear the infoview and it would be confusing.

[Eric Wieser]

Andrew Yang said:

but they will still both appear the infoview and it would be confusing.

Especially since they appear as sorry...

[Eric Wieser]

I take back my suggestion, protected is useless here, also because of ambiguity

[Yaël Dillies]

Why is protected useless? Do you mean open CategoryTheory (Ring) is useless instead?

[Kevin Buzzard]

𝕽𝖎𝖓𝖌?

[Scott Carnahan]

Rings?

[Joël Riou]

No, Rings does not look good to me, because R : Rings could be read as "Let R be a rings" which is grammatically wrong. When we define the category of functors (for which there is a notation, but the same would apply to other categories), the corresponding type is Functor, not Functors.
It seems to me the best solution is the status quo.

[Eric Wieser]

Where the status quo is "randomly decide between *Cat or dropping letters"?

[Andrew Yang]

I believe the status quo is *Cat for algebraic categories. *Grp is the only exception here (which we should change).

[Eric Wieser]

So "an extrapolation of the majority of the status quo" as opposed to the actual status quo? I just wanted to check if @Joël Riou indeed is in favor of renaming Grp et al.

[Andrew Yang]

Although I personally think the *Cat names are perfectly fine, here's a nice thing we could have with notations: We can finally write R-𝐌𝐨𝐝 instead of ModuleCat R for left modules (which is somewhat confusing)

[Joël Riou]

Eric Wieser said:

So "an extrapolation of the majority of the status quo" as opposed to the actual status quo? I just wanted to check if Joël Riou indeed is in favor of renaming Grp et al.

No, I do not want to insist on reverting Grp to the name GroupCat used during the port. What I want to make clear is that I am against the names Rings or Ring, whether in a namespace or not (similarly as I would not like Groups or Group, etc.).

[Eric Wieser]

Andrew Yang said:

We can finally write R-𝐌𝐨𝐝 instead of ModuleCat R for left modules (which is somewhat confusing)

This is no more confusing that it is outside category theory, is it?