Ordinals are everywhere

Stream: mathlib4

[Kevin Buzzard]

@Eric Wieser and I were discussing ordinals and cardinals recently, and he made the observation that cardinals are everywhere in mathlib because we've used them in our definition of dimension. I said that probably mathlib could have got away with a far weaker definition being valued in WithTop Nat and he said that although this might be true, cardinals are not going to be extracated now, so they really play quite a big role in mathlib.

However we both suspected that ordinals played a far lesser role. Indeed I conjectured that ordinals would be used basically nowhere, because mathematicians use Zorn's lemma in practice rather than ordinal induction. I knew of only one proof in mathlib which used ordinal induction, namely N\"obeling's theorem (and I'm off to Copenhagen on Thursday to examine the PhD thesis). Our conversation prompted me to look at the file, and I was fully expecting to see some Import Mathlib.Ordinal type thing at the top, but I was surprised not to see this. Turns out ordinals are imported in Mathlib.LinearAlgebra.Dimension.Free (even though they're never mentioned in that file), indeed they're even imported in Mathlib.LinearAlgebra.FreeModule.Finite.Basic and in Mathlib.RingTheory.Finiteness.Cardinality (again even though they're never mentioned).

The reason they're so ubiquitous is that they're used in Mathlib.SetTheory.Cardinal.Cofinality -- the cofinality of a cardinal is defined to be the cofinality of the corresponding ordinal -- and cofinality of a cardinal is used to deduce various infinite pigeonhole principles which are used in various places. I wondered whether we could move the pigeonhole principles earlier and somehow avoid ordinals being imported everywhere but in 20 minutes of playing around I decided that actually they'd got really embedded. I don't think it's worth removing them -- there are only a couple of ordinal files so we wouldn't win much -- this post is really just to say "huh, ordinals are imported all over the place, I am quite surprised".

[Floris van Doorn]

I'm not surprised. Another reason that ordinals are imported is that the proof of docs#Cardinal.mul_eq_self uses ordinals.

[Joël Riou]

The small object argument and its application to the existence of enough injectives in Grothendieck abelian categories is another significant situation where ordinals (and regular cardinals) appear in mathlib, through definitions by transfinite induction (and this is not a mathlibism: ordinals already appeared in the corresponding original papers/books by Baer, Cartan-Eilenberg and Grothendieck).

[Kevin Buzzard]

There seemed to be uses of countable ordinals in measure theory as well. I remember being told by my measure theory lecturer that "there was no formula for a general Borel set" and then being told by a logician that the measure theory lecturer should learn about countable ordinals.

[Yury G. Kudryashov]

I have a plan to redefine ENat.card without cardinals, but can't find time to do it.

[Peter Nelson]

Yury G. Kudryashov said:

I have a plan to redefine ENat.card without cardinals, but can't find time to do it.

Can you elaborate on the plan?

[Yury G. Kudryashov]

Define ENat.card (α : Sort*) as if Finite α then (Finite.exists_equiv_fin α).choose else \top, then prove its properties and use it w/o Cardinals.

[Yury G. Kudryashov]

I have a draft somewhere.

[Yury G. Kudryashov]

I can have a look later tonight.

[Kyle Miller]

A definition that works and has few prereqs is best, but this might be an interesting definition:

def card (α : Type*) : ℕ∞ :=
  sSup ((↑) '' {n : ℕ | Nonempty (Fin n ↪ α)})

The set in question is an order ideal too. There's some theory here about how ℕ∞ represents order ideals of ℕ.

[Peter Nelson]

I think that ENat and encard provide a happy median between finite and infinite cardinalities in a few places. In some places, it's even the right thing mathematically - it is the most general setting where every matrix has rank equal to that of its transpose, and also where matroid rank makes sense.

But more practically, universe stuff with cardinals, the mess of juggling Finite/Fintype assumptions, andNat-valued cardinality functions with junk values are all annoying in different places. ENat is the place where all of these things go away.

It's surprising to me, for instance, that there is no lemma currently in mathlib stating that the ENat-valued cardinality of a linearly independent family of vectors is at most (some version of) the ENat-valued rank of their span. One has to go through cardinal lifts, OrderHom.mono and Cardinal.toENat to prove this. And PRing something like this feels a bit ad hoc without a proper ENat-valued rank definition.

[Peter Nelson]

#22615 - there is an attempt at something using @Kyle Miller 's definition (WIP). It proves all the existing ENat.card lemmas that don't relate explicitly to cardinals.