lifting to a bigger universe

Stream: new members

[Patrick Lutz]

If I have a theorem proved for objects that are required to be in the same universe and I now have two objects of different universes, how can I apply the theorem? I believe I should be able to use the fact that universes are cumulative to say that both objects are really in the max of the two universes, but I don't know how this is supposed to work.

Here's a mwe of the kind of thing I would like to be able to do

import algebra.field ring_theory.algebra

universes u v

constant p (F : Type u) [field F] (E : Type v) [field E] : Prop
axiom p_of_algebra (F E : Type u) [field F] [field E] [algebra F E] : p F E

example (F : Type u) [field F] (E : Type v) [field E] [algebra F E] : p F E := sorry

[Reid Barton]

It's not true in this much generality. For example p can express that u and v are the same universe (I can explain how to do this if you are curious). You need to make use of the definition of p somehow.

[Reid Barton]

Probably you will have to prove a theorem along the lines of p F E iff p (ulift F) (ulift E).

[Reid Barton]

Well, simpler than my original idea is just

def p (F : Type u) [field F] (E : Type v) [field E] : Prop := nonempty (Type u ≃ Type v)

[Patrick Lutz]

How hard is it to prove something of the form p F E \iff p (ulift F) (ulift E)? The case where I would actually like to do this is for the primitive element theorem. But right now I don't even really know how to consistently get Lean to recognize that ulift F is a field

[Mario Carneiro]

not hard at all, if ≃ is equiv

[Mario Carneiro]

that's just a couple compositions with equiv.ulift

[Patrick Lutz]

Mario Carneiro said:

not hard at all, if ≃ is equiv

I don't really know what this means

[Mario Carneiro]

oh wait, I misread, I thought that the definition said F ≃ E

[Mario Carneiro]

p F E \iff p (ulift F) (ulift E) is obviously false if p asserts that they are the same universe

[Mario Carneiro]

assuming that is p F E \iff p (ulift.{u u'} F) (ulift.{v v'} E)

[Patrick Lutz]

Mario Carneiro said:

p F E \iff p (ulift F) (ulift E) is obviously false if p asserts that they are the same universe

yeah, that's what Reid said

[Patrick Lutz]

But I want to do this in a case where it's true (and I can prove it's true, but only in a complicated way).

[Patrick Lutz]

Specifically for the primitive element theorem

[Mario Carneiro]

What are you trying to do? You can use ulift to put them both in a common universe

[Reid Barton]

It depends on what p is of course--one would imagine there is a large class of such p for which the proof could be produced automatically somehow, but I'm not sure what exactly that class is. I'm also not aware of any example of someone trying to prove a statement like this.

[Reid Barton]

It's basically a souped-up version of equivalence under isomorphism

[Mario Carneiro]

You can prove p (ulift.{u (max u v)} F) (ulift.{v (max u v)} E), because this is just Type (max u v) ≃ Type (max u v)

[Patrick Lutz]

The specific case I want to do is here

[Patrick Lutz]

I want to know if there's an easier way to do it

[Mario Carneiro]

I don't see any universes in that code so it's hard to see what the issue is without compiling

[Reid Barton]

This looks easier than what I had in mind

[Reid Barton]

well, unless you had to write inclusion.separable, inclusion.finite_dimensional etc. and you are counting that as part of the work

[Kevin Buzzard]

@Patrick Lutz why don't you just work with one universe u everywhere? That's what mathematicians have been doing for centuries

[Patrick Lutz]

Reid Barton said:

well, unless you had to write inclusion.separable, inclusion.finite_dimensional etc. and you are counting that as part of the work

We did.

[Patrick Lutz]

Kevin Buzzard said:

Patrick Lutz why don't you just work with one universe u everywhere? That's what mathematicians have been doing for centuries

We were just following the conventions in mathlib.

[Kevin Buzzard]

I've seen people breaking these conventions for reasons very similar to what you are experiencing

[Kevin Buzzard]

Just to be clear -- I mean within mathlib

[Kevin Buzzard]

The computer scientists aren't going to be using the primitive element theorem and the mathematicians live in type if they're doing field theory so I have never seen the use of being maximally polymorphic in situations where there is more than one universe and you're reasoning

[Kevin Buzzard]

Am I right in thinking that bilinear forms need the spaces to be in the same universe for some reason?

[Reid Barton]

It's pretty hard to imagine using the primitive element theorem when the fields are in different universes, especially considering that one is finite dimensional over the other.

[Patrick Lutz]

I guess we might as well keep the current proof though since we've already done it (and the version I linked to is not the main one, it's from a branch where I was trying to get rid of all the stuff like inclusion.separable to make things simpler)