2
$\begingroup$

Before Mathlib 4 was finished, I decided to implement my own ordinals, but this was as I was learning Lean 4, so my Ordinal type had type Type 1 instead of the proper Type u + 1. Now I'm trying to rewrite my code to use as much of Mathlib as possible, and make it as general as possible. I have a function

def ordinalMap.notInjection
  (f: Ordinal → T)
:
  ¬ isInjection f
:=
  ...

and to make it general, the variable T should be able to live in different universes. The problem is that if I just add two universe variables like this:

def ordinalMap.notInjection.{u,t}
  {T: Type t}
  (f: Ordinal.{u} → T)
:
  ¬ isInjection f
:=
  ...

the theorem becomes false -- even the identity function on ordinals is a counter-example. The statement is only true if T has a smaller universe level than (or equal to?) that of the ordinals. (For the proof I adapted the reasoning I found on Wikipedia's article on the Hartogs number. Intuitively, there is always "more ordinals" of Ordinal: Type u + 1 then of objects of T: Type u).

I tried adding this constraint as an argument to the function:

def ordinalMap.notInjection.{u,t}
  {tu: t < u}
  ...

but I get the error "typeclass instance problem is stuck, it is often due to metavariables".

Then I tried to make the type of f Ordinal.{max u (t + 1)} → T, which I suppose would work, but it makes u not necessarily the universe level of the ordinals. Is this the right approach? Or is there something better?


(Lastly, if this function is implemented already somewhere in Mathlib, or can be easily proven using it, I'll be glad to know. I'm afraid I'm not (yet?) very effective at searching in the library.)

$\endgroup$
3
  • $\begingroup$ A MWE might be helpful here complete with the definition (or imports) of Ordinal. But also I guess it is not clear how you hope to use a universe polymorphic version of the ordinalMap.notInjection theorem. (Side note: calling it a definition is confusing.) Without an application in mind, I’m not sure if you can know the right approach. But maybe the right approach is just your original ordinalMap.notInjection theorem. If one has specific universes v < u, they can just ulift T: Type v to Type u and then use your theorem, no? $\endgroup$
    – Jason Rute
    Dec 10, 2023 at 13:06
  • 1
    $\begingroup$ ULift: leanprover-community.github.io/mathlib4_docs/Init/… $\endgroup$
    – Jason Rute
    Dec 10, 2023 at 13:09
  • $\begingroup$ Oh, sorry I thought your original was universe polymorphic but with only one universe variable u, used for both Type and Ordinal. I guess that is what I was suggesting, but the last option also makes sense. I think those are your two options. $\endgroup$
    – Jason Rute
    Dec 10, 2023 at 13:12

1 Answer 1

2
$\begingroup$

I found the versions already in Mathlib. (I used moogle.ai to find it.)

The one universe variable version:

theorem not_injective_of_ordinal {α : Type u}  (f : Ordinal.{u} → α) :
¬Function.Injective f

The two universe variable version:

theorem not_injective_of_ordinal_of_small {α : Type v}  [Small.{u, v} α] (f : Ordinal.{u} → α) :
¬Function.Injective f

Notice how they use the type class Small to handle comparing universe levels.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.