Generalizing normal functions

Stream: maths

[Violeta Hernández]

I've been thinking on and off for the past few days about generalizing docs#Ordinal.IsNormal to functions with arbitrary (well-ordered) domain and codomain.

[Violeta Hernández]

The motivation here is that there are some functions, particularly between ordinals and cardinals, which are morally normal but which we can't currently state as such. These are:

• docs#Cardinal.ord
• docs#Cardinal.aleph (and docs#Cardinal.preAleph)
• docs#Cardinal.beth

[Violeta Hernández]

This generalized definition could also potentially be useful in results about cofinality. The cofinality of a well-order α is the least ordinal o such that there exists a normal function Iio o → α with unbounded range.

[Violeta Hernández]

Likewise, if for whatever reason we want to talk about club sets in arbitrary well-orders, we can show they're precisely the ranges of unbounded normal functions.

[Violeta Hernández]

Now, the thing about doing this generalization is that it opens up a whole can of worms about whether it even makes sense to have normal functions, since they're exactly the same as strictly monotonic continuous functions (wrt the order topology).

[Violeta Hernández]

Maybe it's undesirable to have ordinals importing topology? But on the other hand, defining normal functions like this avoids a bunch of duplication: it'd become much simpler to prove that normal functions commute with suprema, or that the composition of normal functions is normal.

[Violeta Hernández]

Moreover, talking about continuous functions in general means we can also talk about (non-strictly) monotonic continuous functions, which appear for instance as ordinal collapsing functions (something I'm working on in my own repo)

[Violeta Hernández]

It seems perhaps more elegant to show that e.g. multiplication is always continuous on the right, instead of proving it's normal on the right for a non-zero left argument.

[Violeta Hernández]

@Nir Paz Thoughts?

[Daniel Weber]

Are ordinals imported in many files that don't currently import topology? What is the impact of importing Topology.Algebra.Monoid in SetTheory.Ordinal.Arithmetic, for example?

[Kim Morrison]

That seems likely to be a bad idea.

[Daniel Weber]

Yeah, it seems fairly bad, see #19320 (it also violates the two assert_not_exists there)

[Daniel Weber]

Although I don't know how many of these files actually depend on Ordinal.IsNormal - perhaps that could be split into a separate file, which would then import topology?

[Violeta Hernández]

A lot of ordinal arithmetic depends on normal functions.

[Violeta Hernández]

Although, not many applications of ordinals depend on ordinal arithmetic beyond perhaps basic sums and products.

[Violeta Hernández]

Currently SetTheory.Ordinal.Arithmetic is a monolith of a file, containing the basic results of ordinal arithmetic but also the definition of omega0 and lemmas on the lattice structure of ordinals.

[Violeta Hernández]

omega0 (at least the basic results) can likely be moved to SetTheory.Ordinal.Basic, while most of the lattice stuff is in some step of being completely deprecated or generalized.

[Violeta Hernández]

I think it'd be interesting to see how many files still need ordinal arithmetic after finishing this whole refactor business. Ideally I'd expect nothing beyond more ordinal arithmetic to depend on it.

[Kevin Buzzard]

Is one solution simply to split SetTheory.Ordinal.Arithmetic into the "simple" part (ie .Basic) and the more technical part? (Oh -- Daniel already suggested this, sorry)

[Violeta Hernández]

Violeta Hernández said:

A lot of ordinal arithmetic depends on normal functions.

Perhaps our current proofs rely on it too much, though. For instance docs#Ordinal.mul_le_mul_iff_left uses that multiplication is normal when really it should be possible to prove it at the relation embedding level.

[Nir Paz]

I of course don't like the idea of normal functions being defined topologically, but there's no need to repeat that discussion haha.

For the suggestion, I agree it would be nice to state all these function are normal directly, just like the omega function simplified all the normality arguments about the aleph function.

But all the recent iSup-Small api is specific for ordinals, right? It's a bit sus to add a definition that talks about iSup to arbitrary well orders, without them having the api to reason about iSup very well.

[Nir Paz]

Oh I just looked, normal functions don't use iSup in the definition. But it is often something you use to work with them.

[Daniel Weber]

Perhaps we could have a SetTheory.Ordinal.Topology file which shows the equivalence of IsNormal to being continuous and strictly monotonic, and that addition and multiplication are continuous

[Violeta Hernández]

We already have a SetTheory.Ordinal.Topology file that proves the equivalence of IsNormal to being continues and strictly monotonic :smile:

[Violeta Hernández]

docs#Ordinal.isNormal_iff_strictMono_and_continuous

[Violeta Hernández]

We don't prove addition and multiplication are continuous because they're not. They're just continuous on the right.

[Yury G. Kudryashov]

It would be nice to have parts of the ordinal arithmetic that are needed for cardinal arithmetic with minimal dependencies. IMHO, cardinal arithmetic is what matters most in other parts of the library (e.g., dimensions etc), while advanced ordinal arithmetic is used much less in the library (am I wrong?)

[Violeta Hernández]

I opened #20504 where I "generalize" normal functions to functions between well-orders. Even if the intended definition of normal functions is just "strictly monotonic and continuous" I think it's fine to collect all the other standard (and often more useful) definitions in terms of least upper bounds / suprema into their own predicate.