HasULift typeclass

Stream: mathlib4

[Violeta Hernández]

In #19959, @Joël Riou defines a HasCardinalLT predicate for types and cardinals within distinct universes, for the purposes of using it within category theory. I'm wondering if we can implement this idea in more generality.

Here's what I'm thinking: define a HasULift a b c typeclass for types a, b which embed as an initial segment of c. The intended implementers would be a = Cardinal.{u}, b = Cardinal.{v}, and c = Cardinal.{max u v} (as well as ordinals!). We can then define universe polymorphic equality and ordering between types a and b, and prove results like antisymmetry, transitivity, and whatnot.

This would be a pretty big refactor, since at the moment a lot of results are stated using the Cardinal.lift{v} a = Cardinal.lift{u} b pattern, but it would have some benefits:

• more readable code that isn't littered with lift
• we don't have to duplicate theorems by having lift and non-lift versions, since we can instead just write them using the universe polymorphic order predicates instead
• we sidestep existing issues with simp and lift (at the moment simp can't do simplifications like lift.{max u v, u} = lift.{v, u})

[Joël Riou]

Again, I do not want to disturb the set theory API (for the limited use of which I have experienced very good behaviour of simp). The HasCardinalLT predicate is needed for the study ofκ-filtered categories for a regular cardinal κ (they are a generalization of filtered categories, and they will be used when proving for example that Grothendieck abelian categories have enough injectives), and there is no particular reason it would be used extensively outside of category theory. Then, I do not think any refactor is necessary.

[Violeta Hernández]

I don't really see a reason for this predicate to be any more useful in the context of category theory than outside of it. If working with lift directly is troublesome, then my proposed refactor should be useful throughout Mathlib. If it's not, then I don't think the HasCardinalLT predicate is necessary.

[Joël Riou]

I can assert it is useful in the context of category theory!

[Dagur Asgeirsson]

Joël Riou said:

I can assert it is useful in the context of category theory!

I think this :this: outweighs any considerations of refactoring the set theory API.
I've left an approving review but I wanted to give @Violeta Hernández a chance to respond before maintainer merging

[Violeta Hernández]

I do agree that this sort of ambitious refactor shouldn't hold up mathematical work. So I agree with this being merged as is.

[Violeta Hernández]

I do still think it can potentially be something to work on. If a simple cardinal inequality is inconvenient enough that it's useful to introduce API on top of that, then maybe that's true of the entire lift API too.

[Violeta Hernández]

I'll do the HasULift experiment as a draft PR. That should allow us to judge if I'm onto something.