Naming convention: topological spaces

Stream: mathlib4

[Michael Rothgang]

What's the preferred naming convention for topological spaces? Currently, I mostly see Greek letters $\alpha$, $\beta$, $\gamma$. From math textbooks, I'm much more used to letters $X$, $Y$, $Z$ etc.

Per the style guide, one may think the latter is preferred and the former mostly pre-existing/local consistency/inertia. Maybe this is wrong. Let me know what you think!

[Patrick Massot]

Greek letters come from the antiquity of Mathlib. $X$, $Y$ and $Z$ are now preferred.

[Kevin Buzzard]

Greek letters were the preferred naming convention for everything in 2017 :-) but we complained enough and they changed the convention :-)

[Eric Wieser]

I'd claim they're still preferred for plain types with no typeclasses?

[Eric Wieser]

(as that's what https://leanprover-community.github.io/contribute/naming.html#variable-conventions implies)

[Eric Wieser]

(though frankly I don't think that section aligns very well with mathlib; I can't remember the last time i j k were integers)

[Michael Rothgang]

Thanks for the clarification. First two PRs sent as #7587 and #7589.

[Yaël Dillies]

Greek letters are still very much preferred for many things, Patrick :thinking:

[Johan Commelin]

@Yaël Dillies Citation needed. I think some people adapted to the old convention. But I don't know of any informal-maths reference text that uses $\alpha, \beta, \gamma$ for "universal sets" or types. Not in topology, not in order theory, not in algebra, etc...

[Yaël Dillies]

Okay here's a concrete example where the "old" convention would be better: docs#AddChar

[Yaël Dillies]

Michael Stoll writes that "the definition works for R an additive commutative monoid and R' a commutative monoid, but we will soon restrict to them being rings". Hence the name of the variables.

[Kevin Buzzard]

That looks like a fine convention to me. Are you saying that alpha is better?

[Kevin Buzzard]

The only uses of AddChar in the wild have commrings as source and target

[Yaël Dillies]

However, in LeanAPAP, we use AddChar for R an additive group and R' a ring. Which would warrant AddChar G R rather than AddChar R R'. So now I'm faced with either having R standing for a group, or with dully renaming all the variables in the file. If we had used α, β from the onset, I wouldn't need such a stupid diff.

[Kevin Buzzard]

Alpha would still be worse because then nobody has a clue what's going on

[Damiano Testa]

As someone who learned informal maths way before any formalized one, it took some time to get adjusted to greek letters for type. I find it an acceptable convention now, if you do not want to convey any expectation on the type, but I do not think that I ever saw it in informal maths.

[Yaël Dillies]

Also α is a great convention in combinatorics where everybody write $$X ⊂ 2^[[n]}$$ and you certainly don't want a type called $[n]$ (nor Fin n since that would be ordered and work badly with induction).

[Johan Commelin]

Yaël Dillies said:

However, in LeanAPAP, we use AddChar for R an additive group and R' a ring. Which would warrant AddChar G R rather than AddChar R R'. So now I'm faced with either having R standing for a group, or with dully renaming all the variables in the file. If we had used α, β from the onset, I wouldn't need such a stupid diff.

I think renaming the variables is the correct move (-; I'm aware that this is a matter of taste. But I'd argue that these variable names carry semantic value. Similarly, it would be really confusing if we started doing $\epsilon$-$\delta$-proofs with $x,y$, just because "that's what real numbers are always called".

[Johan Commelin]

So really, while I understand your frustration, I don't think that "renaming variables diff" would be "stupid". Because it demonstrates that we learned that AddChar is used in more general contexts, and hence Stoll's documentation also can be updated. We learned something!

[Kevin Buzzard]

Why not use $A$ for $R$ @Yaël Dillies ? Because this is nicely ambiguous -- could be an additive abelian group, could be a ring.

[Michael Stoll]

Yaël Dillies said:

Okay here's a concrete example where the "old" convention would be better: docs#AddChar

I'm to blame for that. They used to be rings... :smile:
(OK; I now see that Yaël has already mentioned this -- I should remember reading the thread to the end before replying...)

[Yaël Dillies]

I mean, sure, if you are to merge the PR that renames the variables.

[Johan Commelin]

If such a PR exists, I apologize for missing it. Can you please give me a pointer?

[Michael Rothgang]

Michael Rothgang said:

Thanks for the clarification. First two PRs sent as #7587 and #7589.

After merging master, now #7587 fails to build - I'm rather puzzled by the error. Help welcome &appreciated.

[Michael Rothgang]

After merging master, now #7587 fails to build - I'm rather puzzled by the error. Help welcome &appreciated.
Thanks for the help with fixing this.

Can somebody re-bors this PR, please? I had pushed to it after it was r+-ed, to fix a conflict that was not visible to git. Apparently, it's fallen through the cracks now.

[Michael Rothgang]

#7591 is the third PR along these lines.