Ordinal.lsub

Stream: maths

[Violeta Hernández]

Out of all of my planned refactors on ordinals, the docs#Ordinal.lsub refactor is the one I'm the most iffy about.

[Violeta Hernández]

There's a few issues with lsub. One is the name, which is a bit obscure without the docstring (it stands for least strict upper bound). Of course, there's also the issue with universes - if we are to keep this function, we should not restrict the universes of the indexing family.

[Violeta Hernández]

But the greater issue is that using lsub instead of writing its definition down explicitly means we can't use the vast API that already exists for suprema.

[Violeta Hernández]

On the other hand... this is definitely a useful definition to have. It appears most prominently in cofinality: the cofinality of an ordinal o is the smallest cardinal of an indexing family f : ι → Ordinal with lsub f = o.

[Violeta Hernández]

What should be done? I see three options here:

[Violeta Hernández]

/poll What to do with lsub?
Deprecate lsub, use iSup
Keep lsub (but generalize its universes)
Generalize lsub to appropriate typeclasses

[Violeta Hernández]

The generalization option would be really cool, but it comes with a high maintenance cost. And there's the issue of whether we should also have a set version...

[Violeta Hernández]

I'm pretty much 50/50 on deprecating or keeping it.

[Violeta Hernández]

(In any case, docs#Ordinal.blsub has to go)

[Violeta Hernández]

@Yaël Dillies @Nir Paz

[Nir Paz]

Adding an explicit succ ∘ in the characterization of cofinality isn't that bad, especially since for limits it's equivalent to iSup. This is always the interesting case so I assume the clumsier iSup (succ ∘ f) won't even be used often.

[Violeta Hernández]

Not quite, every nonzero ordinal is the supremum of a singleton (namely the one consisting of itself)

[Violeta Hernández]

On the other hand, it's true that you can just characterize the cofinality of a limit ordinal as the size of the least set of smaller ordinals whose supremum equals it

[Violeta Hernández]

Well the poll clearly shows we don't want this haha

[Violeta Hernández]

I'll try to refactor the cofinality file to not use lsub in the coming weeks

[Violeta Hernández]

Its other uses are somewhat more minor - after getting rid of those we can deprecate the function altogether