Domain-specific type names

Stream: mathlib4

[Yury G. Kudryashov]

Where should we codify domain specific preferred type names? Currently, #naming says

Types with a mathematical content are expressed with the usual mathematical notation, often with an upper case letter (G for a group, R for a ring, K or 𝕜 for a field, E for a vector space, ...). This convention is not followed in older files, where greek letters are used for all types. Pull requests renaming type variables in these files are welcome.

but different people have different opinions on what letters should we use in various cases. Once we decide, e.g., that topological/uniform/metric spaces without algebraic or order structure are named X, Y, Z (BTW, what if I need more letters here? Indexes/primes? Other Latin capital letters?), should we add this information to #naming or to a README.md file in the corresponding folder?

[Yury G. Kudryashov]

The main issue with adding everything to #naming is that this section can grow large, with most information irrelevant to most readers.

[Yury G. Kudryashov]

Also, I have some specific questions about naming variable types:

• do we continue using lowrecase Greek letters for measurable/measure spaces, or do we switch to something else?
• what do we use for types with Preorder/PartialOrder/LinearOrder, with or without extra structures (topology, σ-algebra) compatible with the order?
• If a file deals with modules, it's common to use R fo rthe ring and M, N for the modules. What if a lemma gets generalized from [Semiring R] [Module R M] to [Monoid R] [MulActionWithZero R M] or even [SMul R M]? Should we use another variable instead of R? In case of a monoid, an obvious choice would be M, but it conflicts with M for the module.
• What do we use for fields: k, K, or \bbk? How do we choose between these?
• What do we use for types with [DivisionMonoid _] [HasDistribNeg _]? The main users are fields, but there may be other types satisfying these assumptions (e.g., products of fields).

[Yury G. Kudryashov]

@Yaël Dillies I know that you often have an opinion on questions like these :up:, wdyt?

[Michael Rothgang]

Big :+1: for documenting this (having #naming explicitly point to directory READMEs is fine with me)

[Yury G. Kudryashov]

What I currently know:

• Monoids: M, N, P
• Groups: G, H, K
• Monoids with zero or groups with zero: same with ₀
• (Semi)rings: R, S, T
• Fields: k, K, L, \bbk depending on the file;
• modules: M, N
• vector spaces, normed groups: E, F, G
• topological spaces, uniform spaces, metric spaces: X, Y, Z
• lattices: L (I saw this in some files, have no stats about that)
• categories: C, D

[Johan Commelin]

I think we should add this list of letters as "strong recommendation" and "typical examples", but ultimately there will always be exceptions and edge cases. Mainly we want to encourage following existing conventions in the usual literature. And leave edge cases to the wisdom of capable authors and reviewers.

[Kevin Buzzard]

The clash with M for both monoid and module has always irked me to the extent that I've often used A for modules (because they're abelian). It's also common to use A for algebras (which irks me because now we have two uses for A instead of two uses for M)

[Bryan Gin-ge Chen]

Maybe we could add these naming suggestions to the docstring of the type? That way the suggested name is only a hover away.

[Yaël Dillies]

Yury G. Kudryashov said:

What I currently know:

• Monoids: M, N, P
• Groups: G, H, K
• Monoids with zero or groups with zero: same with ₀
• (Semi)rings: R, S, T
• Fields: k, K, L, 𝕜 depending on the file;
• modules: M, N
• vector spaces, normed groups: E, F, G
• topological spaces, uniform spaces, metric spaces: X, Y, Z
• lattices: L (I saw this in some files, have no stats about that)
• categories: C, D

To compare, this is what I use:

• Monoids: M, N, O
• Groups: G, H
• Monoids with zero: M₀, N₀
• (Semi)rings: R, S
• Fields: K or 𝕜
• Modules, vector spaces: M, N, O
• Normed groups: E, F, G
• Inner product spaces: H
• Topological spaces, uniform spaces, metric spaces: X, Y, Z
• Preorders, partial orders, etc...: α, β, ...
• Categories: C, D, E

[Yaël Dillies]

Yury G. Kudryashov said:

• What do we use for types with [DivisionMonoid _] [HasDistribNeg _]? The main users are fields, but there may be other types satisfying these assumptions (e.g., products of fields).

Division monoids are group-like to me, so G, H. HasDistribNeg is ring-like to me, so R, S