Matroid rank - naming poll

Stream: mathlib4

[Peter Nelson]

This stuff is on its way from my repo to mathlib, and so for the sake of planning ahead, I wanted to solicit a consensus.

A matroid M : Matroid α is a certain structure on a type α with a distinguished 'ground set' M.E : Set α.
For each X : Set α, there is a notion of the 'rank of X in M, which generalizes the usual rank in linear algebra. The 'rank of M' refers to the rank in M of the set M.E.

In various settings, it is reasonable for rank to take values in ℕ, ℕ∞ and Cardinal.
All three versions are useful. The ℕ version, in particular, is all that is used in 95% of the literature, the ℕ∞ version is far less common but is needed for formalizing infinite matroids, and the Cardinal version is even less common (and not well-defined for all matroids), but has some applications. It is also very helpful to refer to the 'rank of a matroid' separately from just saying 'rank of the ground set in the matroid'. This means, in practice, that the following things need names:

• a term Matroid α → ℕ assigning each matroid its rank as a natural number.
• a term Matroid α → ℕ∞ assigning each matroid its rank as an extended natural number.
• a term Matroid α → Cardinal assigning each matroid its rank as a cardinal.
• a term in Matroid α → Set α → ℕ assigning each set to its ℕ-valued rank in a matroid
• a term in Matroid α → Set α → ℕ∞ assigning each set to its ℕ∞-valued rank in a matroid
• a term in Matroid α → Set α → Cardinal assigning each set to its Cardinal-valued rank in a matroid.
• certain typeclasses in Matroid α → Prop stating a matroid's rank is finite/infinite/positive.

The current terms in my repo are

• Matroid.rk (M : Matroid α) : ℕ
• Matroid.erk (M : Matroid α) : ℕ∞
• nothing yet for cardinal rank
• Matroid.r (M : Matroid α) (X : Set α) : ℕ
• Matroid.er (M : Matroid α) (X : Set α) : ℕ∞
• nothing yet for cardinal rank of sets
• FiniteRk, RkPos, etc for typeclasses.
  (Also already in mathlib, but can be changed without too much hassle)

I've favoured short names here, especially for the functions on sets, because they are ubiquitous in calculations, and because r is the usual pen-and-paper notation for all notions of rank. But perhaps notation that terse is bad for other reasons. A poll follows with some options. (The Matroid namespace is assumed)

[Peter Nelson]

/poll How should matroid rank terms be named?
rk, erk, cardrk for the terms, r, er, cardr for the set functions, FiniteRk etc for the typeclasses
rank, erank, cardRank for the terms, rk, erk, cardRk for the set functions, FiniteRank etc for the typeclasses
Something else

[Eric Wieser]

I guess the closest comparison would be Module.rank and Module.finrank. I'm curious if you can make do without the ENat version, since we were able to make do without it for linear algebra. If both ENat and Cardinal are rare, then the slight pain of using the cardinal one for the enat case shouldn't come up enough to matter.

[Eric Wieser]

Is M.rk the same thing as M.r univ, using the names in your initial message?

[Peter Nelson]

Eric Wieser said:

Is M.rk the same thing as M.r univ, using the names in your initial message?

Yes, but also M.r M.E, which comes up more.

[Peter Nelson]

The ENat version is needed, because (for instance), it is consistent with ZFC that there are matroids having both a countable basis and an uncountable basis.

This means that cardinal rank, even if defined as a supremum or infimum of the cardinalities of bases, will not have nice properties at the full generality of matroids (as a concrete example, things like monotonicity, or the statement that $r(X) = r(\mathrm{closure(X)})$ will be unprovable in general).

[Eric Wieser]

If you have a cardinal-valued cardinality, you can always use toENat on the result

[Peter Nelson]

That's right - the cardinal expression is ok as a definition, but you can't prove anything nice about it, so all the proofs happen in ENat anyway.

[Eric Wieser]

It's ok to prove things about (rank M).toENat without creating a new definition though, especially given you claim the cases where this arises are rarer

[Peter Nelson]

I meant that they are rare in the literature. ENat-valued rank is all over the place when formalizing, to maintain generality.

[Eric Wieser]

I'm afraid through my own ignorance I don't understand the comment about why the cardinal-valued statements are poorly behaved; they work quite well for us in linear algebra. Is there some nice intuition for why this doesn't successfully generalize to matroids?

[Peter Nelson]

I guess 'infinite matroids are too wild' is the only real answer. Higgs proved that if the generalized continuum hypothesis holds, then cardinal-valued rank is well-behaved (i.e. all bases are equicardinal), and it is known that bases are equicardinal for certain classes, such as the finitary matroids - and this last result is now in mathlib!

Because of the GCH result, the constructions that show the bad behaviour necessarily involve exotic set-theoretic assumptions like Martin's axiom. I don't have any intuition.

[Peter Nelson]

This is one of the ways that infinite matroids are terrible. But they are surprisingly nice in most ways.

[Kevin Buzzard]

Note that we have docs#Polynomial.degree and docs#Polynomial.natDegree

[Junyan Xu]

@Johan Commelin seems to think we should change docs#Module.finrank, docs#Subfield.relrank, docs#Subfield.relfinrank, and docs#Subgroup.relindex (anything else?) to finRank, relRank, relFinRank, and redIndex according to his vote. Field.finSepDegree already follows this convention. I don't think we're going to change Finset and Fintype though ...

[Yaël Dillies]

Note that I've opened #19872 for a similar rename

[Peter Nelson]

I think I like the extra option that was added (rank, eRank cRank, for the terms, rk, eRk, cRk for the functions).

I would rather not use nat_, fin_ or such variants for the Nat versions, because this will make the statements of real theorems involving the rank function less readable in exactly the setting that they are most common.

[Peter Nelson]

Junyan Xu said:

Johan Commelin seems to think we should change docs#Module.finrank, docs#Subfield.relrank, docs#Subfield.relfinrank, and docs#Subgroup.relindex (anything else?) to finRank, relRank, relFinRank, and redIndex according to his vote. Field.finSepDegree already follows this convention. I don't think we're going to change Finset and Fintype though ...

Would this mean ncard -> nCard and encard -> eCard would be good ideas? @Johan Commelin

[Eric Wieser]

Isn't the argument for encard vs enCard the same as the argument for ennreal vs ennReal in theorem names?

[Edward van de Meent]

or eNNReal? :upside_down:

[Peter Nelson]

I don't think there was much of a naming discussion about encard when I made the PR. But would it be enCard or eNCard according to the new rules?

[Eric Wieser]

I don't think the rules are clear here

[Edward van de Meent]

i'd say that since we're abbreviating Nat, the n becomes lowercase? (compare to eNatCard).

[Eric Wieser]

Agreed, but I think the rules ought to spell that out

[Peter Nelson]

But the c should still become C, I guess.

[Eric Wieser]

If the rule were "name in CamelCase then lowercase with the normal rules", then you'd have ENCard lowercased to encard.

[Peter Nelson]

Well that's easy, then!

[Yaël Dillies]

Note that some lemmas lower-case AEStronglyMeasurable to aeStronglyMeasurable. Not sure how to feel about those

[Edward van de Meent]

Eric Wieser said:

If the rule were "name in CamelCase then lowercase with the normal rules", then you'd have ENCard lowercased to encard.

i believe actually it is more common for just the first character to become lowercase?

[Edward van de Meent]

see docs#natCast for an example

[Edward van de Meent]

i could also be wrong about that, though...

[Yaël Dillies]

but it's not called NATCast in upper-case?

[Edward van de Meent]

ah, i get what you mean now...

[Peter Nelson]

Can I suggest that those involved in this discussion provide an opinion in the poll at the top? It seems we're heading in the direction of a consensus. (The encard issue is orthogonal)

[Johan Commelin]

Whatever the rules are, we should make sure that we don't end up with crank. I don't care about the rest (-;

[Junyan Xu]

They'll come sooner or later!

[Peter Nelson]

I'll leave this for the weekend, but it doesn't seem like there's much disagreement (a vote or two more would be nice!).

[Junyan Xu]

Yaël Dillies said:

Note that I've opened #19872 for a similar rename

Worth noting there's an objection to such renaming in the PR.