Cardinal.lift as an InitialSeg

Stream: maths

[Violeta Hernández]

In #16347, I make docs#Cardinal.lift an docs#InitialSeg. This is a structure that sees little use in the current API, but I believe doing this has a lot of advantages. I'll paraphrase what I said in that PR.

Most crucially, being an initial segment embedding from Cardinal.{u} into Cardinal.{max u v} is precisely the property that characterizes lift, as it essentially encodes the mathematical intuition that one is "just a subset of the other". As such, most of the order properties of lift, such as docs#Cardinal.lift_lt, docs#Cardinal.lift_succ, docs#Cardinal.lift_iSup, as well as some others like docs#Cardinal.lift_lift and the (to be added) Cardinal.lift_aleph, all follow from this initial segment structure (even if most of these lemmas are still missing in that generality).

The only cons I can see for this change is that dot notation breaks (in exactly two lines of code, mind you), and that the InitialSeg structure might be unfamiliar to people using the API (though conversely, using the structure more should alleviate that).

[Violeta Hernández]

@Yaël Dillies

[Violeta Hernández]

To be clear, if this refactor goes through, I also plan on doing the same with docs#Ordinal.lift

[Eric Wieser]

A pattern sometimes used here is to keep foo around as the simp-normal form, but introduce a fooHom (or here, fooInitialSeg`) to use when building proofs of those theorems

[Violeta Hernández]

I think that pattern is successful when the bundled structure isn't something you necessarily care about, or when it's hard to build it up all at once. I'm arguing this is not one of those cases.

[Eric Wieser]

Often the reason for preferring that pattern is "there are multiple incompatible bundlings possible, so to avoid having to pick a preferred one we prefer the unbundled spelling"

[Violeta Hernández]

I do admit there's one other possible bundling that makes sense, which is a ring homomorphism

[Violeta Hernández]

Or, when the target universe is strictly larger, a principal segment embedding

[Violeta Hernández]

Alright, maybe it does make sense to have the unbundled version separate

[Violeta Hernández]

Should it just be called Cardinal.lift.initialSeg?

[Eric Wieser]

liftInitialSeg is slightly more common

[Violeta Hernández]

I should note docs#Ordinal.lift.initialSeg exists

[Violeta Hernández]

Should that be renamed at some point?

[Violeta Hernández]

Also, here's another question: what about docs#Ordinal.typein ?

[Violeta Hernández]

I think that has a much stronger case for being made into a PrincipalSeg

[Violeta Hernández]

There is no other reasonable structure to give it. No one is using dot notation with this. And also, we didn't have any problem with making docs#Ordinal.enum into a RelIso a month or so ago.

[Eric Wieser]

Violeta Hernández said:

I should note docs#Ordinal.lift.initialSeg exists

In that case being locally consistent is fine.