Naming: singular vs plural

Stream: mathlib4

[Yury G. Kudryashov]

Most names use singular form (Polynomial etc) but there are some exceptions, e.g., docs#Units docs#TopologicalSpace.Opens
Should we rename Units to Unit and Opens to Open or OpenSet? Also, should we move Units/Unit to a namespace? This is a very generic name that a downstream project can use, e.g., to formalize units like "meter", "second" etc.

[Johan Commelin]

It could be UnitGroup...

[Antoine Chambert-Loir]

Unit already exists, doesn't it?

[Yury G. Kudryashov]

Indeed, docs#Unit exists, but is it a good reason to use plural instead of another word?

[Antoine Chambert-Loir]

If you wish for a name, unit is the canonical one and I'm not sure there are other words; if an adjective is ok for you, invertible works well, and predicates are also possible: isUnit or isInvertible.

[Jireh Loreaux]

Personally, I think UnitGroup makes the most sense to avoid name clashes (and it plays well with to_additive, whereas something like Monoid.Unit is worse in this regard).

[Jireh Loreaux]

As for the singular vs. plural issue in general, I don't think we should worry about it too much.

[Eric Wieser]

I don't think AddMonoid.Unit would cause any trouble with to_additive

[Eric Wieser]

But UnitGroup is shorter

[Jireh Loreaux]

Eric, AddMonoid.Unit is fine by itself, but then in all theorems about it we would be forced to include the namespace like monoidUnit or addMonoidUnit. And indeed, UnitGroup is shorter.

[Eric Wieser]

I think actually in many theorem names we could get away with just using unit, since there are unlikely to be many ambiguous cases.

[Jireh Loreaux]

ah, your claim is that to_additive can just map unit to unit and all will be well because somewhere else in the name we have mul (or whatever) that gets sent to add? That seems likely to be true most of the time, but not an ideal strategy.

[Mario Carneiro]

Yury G. Kudryashov said:

Most names use singular form (Polynomial etc) but there are some exceptions, e.g., docs#Units docs#TopologicalSpace.Opens
Should we rename Units to Unit and Opens to Open or OpenSet? Also, should we move Units/Unit to a namespace? This is a very generic name that a downstream project can use, e.g., to formalize units like "meter", "second" etc.

I don't think this is a valid comparison: Polynomial is a predicate-like operation applied to a type, so it is named like an adjective or noun, while Units and Opens are bundled objects (sets or categories) which instead have a membership operation. I think it is a reasonable convention to have e.g. Prime : Nat -> Prop and primes : Set Nat

[Yury G. Kudryashov]

Currently we have docs#Nat.Prime and docs#Nat.Primes

[Yury G. Kudryashov]

The latter is a type, not a set.

[Mario Carneiro]

same idea though

[Yury G. Kudryashov]

But we have docs#Submonoid

[Mario Carneiro]

it's bundled

[Eric Wieser]

I was going to make the same point as Mario, but half as well

[Yury G. Kudryashov]

You don't write s ∈ Opens X, you write s : Opens X.

[Yury G. Kudryashov]

Why Opens is different from Submonoid?

[Yury G. Kudryashov]

Both are bundled sets with extra properties.

[Mario Carneiro]

Because Open X doesn't make sense, open is a verb

[Yury G. Kudryashov]

OpenSet?

[Mario Carneiro]

and even if we ignore that and read open as an adjective, it doesn't apply to X it applies to s

[Yury G. Kudryashov]

Clearly, Opens is a form of the verb "open". Like "he opens the door".

[Yury G. Kudryashov]

s : Submonoid M reads "s is a submonoid of M". We can have U : OpenSet X as "U is an open set in X"

[Eric Wieser]

I think OpenSet would be fine

[Eric Wieser]

But Opens is also fine as is

[Eric Wieser]

UnitGroup is less fine, because u : UnitGroup doesn't mean "u is a unit group"

[Eric Wieser]

"u : Units" is fine because you might say "u is one of the units", but p : Polynomials R is silly because you wouldn't say "p is one of the polynomials over R"

[Eric Wieser]

I don't think any of this is an argument against u : Monoid.Unit M (reading as "u is a unit of the monoid M"), but this "one of the" approach does seem like a reasonable way to justify the status quo.

[Jireh Loreaux]

We should definitely move Units out of the root namespace, or rename it.