# Zulip Chat Archive

## 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