Capitalization of LE/Le

Stream: mathlib4

[Jovan Gerbscheid]

In mathlib there are many definitions that refer to LE/Le in their name. It would be great to make this more consistent. However it isn't quite clear to me what the rules are here.

For types we have Valuation.RankOne.rankLeOneStruct, LeOnePart VS ZeroLEOneClass, Ring.DimensionLEOne, Filter.EventuallyLE

And for definitions we have LieSubalgebra.ofLe, SimplexCategory.mkOfLe VS LocalizedModule.liftOfLE, CategoryTheory.homOfLE

Just to give a few examples.

[Yury G. Kudryashov]

IMHO, LE is the correct spelling if L is capitalized. See docs#ENNReal for a similar example.

[Kenny Lau]

while we're at it, how should we deal with LinearEquiv? Is it Lequiv or LEquiv?

[Jovan Gerbscheid]

cslib was having some similar problems I think :laughing:

[Jovan Gerbscheid]

Yury G. Kudryashov said:

IMHO, LE is the correct spelling if L is capitalized. See docs#ENNReal for a similar example.

I think the reason why people are discarding this rule is that they want word boundaries to be clear. ENNReal is one word and it ends in a lowercase, so there are no issues. But in LEOne, it's not clear where the word boundary is.

[Ruben Van de Velde]

I think a fair number of Le are incorrectly autotranslated from lean 3

[Ruben Van de Velde]

But your point is one reason I haven't gone after them :)

[Yaël Dillies]

Kenny Lau said:

while we're at it, how should we deal with LinearEquiv? Is it Lequiv or LEquiv?

LinearEquiv. It shouldn't be abbreviated further!

[Yaël Dillies]

If that's too long, I am always open to renaming it globally to LinearIso, but that is a lot of churn.

[Yury G. Kudryashov]

We have quite a few definitions abbreviated like myHomCLM etc (myHom bundled as ContinuousLinearMap). Sometimes, unfolding these abbreviations result in really long names.

[Junyan Xu]

If that's too long, I am always open to renaming it globally to LinearIso, but that is a lot of churn.

How about equivₗ, as ₗ is used in the notation. Also in Matrix.toLin etc. Lin is used as a shorthand for LinearMap. Should it be LM?

while we're at it, how should we deal with LinearEquiv? Is it Lequiv or LEquiv?

I just found docs#finsuppLequivDFinsupp and docs#finsuppLEquivDirectSum ...

[Michael Rothgang]

I'll happily review a PR about these two!

[Yury G. Kudryashov]

About equivₗ: I think that suffixes like ₗ/L are worse than LM/CLM. I don't want to rename definitions and lemmas if we ever change notation.

[Yury G. Kudryashov]

(I know that I've introduced some definitions with suffixes like ₗ)

[Floris van Doorn]

Jovan Gerbscheid said:

I think the reason why people are discarding this rule is that they want word boundaries to be clear. ENNReal is one word and it ends in a lowercase, so there are no issues. But in LEOne, it's not clear where the word boundary is.

to_additive special-cases such all-capital names (or names that end in a capital letter). I don't think we should necessarily avoid them.