Zulip Chat Archive

Stream: new members

Topic: lifting to a bigger universe


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 20:59):

not hard at all, if is equiv

view this post on Zulip Mario Carneiro (Aug 12 2020 at 20:59):

that's just a couple compositions with equiv.ulift

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 21:00):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 21:01):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Patrick Lutz (Aug 12 2020 at 21:02):

Specifically for the primitive element theorem

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 12 2020 at 21:02):

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

view this post on Zulip 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)

view this post on Zulip Patrick Lutz (Aug 12 2020 at 21:03):

The specific case I want to do is here

view this post on Zulip Patrick Lutz (Aug 12 2020 at 21:03):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 21:05):

This looks easier than what I had in mind

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:12):

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

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:12):

Just to be clear -- I mean within mathlib

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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