## Stream: new members

### Topic: lifting to a bigger universe

#### Patrick Lutz (Aug 12 2020 at 20:43):

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 (Aug 12 2020 at 20:47):

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 (Aug 12 2020 at 20:48):

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

#### Reid Barton (Aug 12 2020 at 20:52):

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 (Aug 12 2020 at 20:58):

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 (Aug 12 2020 at 20:59):

not hard at all, if ≃ is equiv

#### Mario Carneiro (Aug 12 2020 at 20:59):

that's just a couple compositions with equiv.ulift

#### Patrick Lutz (Aug 12 2020 at 21:00):

Mario Carneiro said:

not hard at all, if ≃ is equiv

I don't really know what this means

#### Mario Carneiro (Aug 12 2020 at 21:00):

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

#### Mario Carneiro (Aug 12 2020 at 21:01):

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

#### Mario Carneiro (Aug 12 2020 at 21:01):

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

#### Patrick Lutz (Aug 12 2020 at 21:01):

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 (Aug 12 2020 at 21:02):

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 (Aug 12 2020 at 21:02):

Specifically for the primitive element theorem

#### Mario Carneiro (Aug 12 2020 at 21:02):

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

#### Reid Barton (Aug 12 2020 at 21:02):

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 (Aug 12 2020 at 21:02):

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

#### Mario Carneiro (Aug 12 2020 at 21:03):

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 (Aug 12 2020 at 21:03):

The specific case I want to do is here

#### Patrick Lutz (Aug 12 2020 at 21:03):

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

#### Mario Carneiro (Aug 12 2020 at 21:04):

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

#### Reid Barton (Aug 12 2020 at 21:05):

This looks easier than what I had in mind

#### Reid Barton (Aug 12 2020 at 21:05):

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

#### Kevin Buzzard (Aug 12 2020 at 21:10):

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

#### Patrick Lutz (Aug 12 2020 at 21:11):

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 (Aug 12 2020 at 21:11):

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 (Aug 12 2020 at 21:12):

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

#### Kevin Buzzard (Aug 12 2020 at 21:12):

Just to be clear -- I mean within mathlib

#### Kevin Buzzard (Aug 12 2020 at 21:13):

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 (Aug 12 2020 at 21:14):

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

#### Reid Barton (Aug 12 2020 at 21:14):

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 (Aug 12 2020 at 21:27):

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)

Last updated: May 17 2021 at 21:12 UTC