Zulip Chat Archive

Stream: general

Topic: ulift tactic


view this post on Zulip Johan Commelin (Oct 15 2020 at 06:51):

How hard would it be to have a ulift tactic+attribute, that takes a goal state and uses everything it knows about ulift to turn it into a goal state where all types live in the same universe?
I'm currently trying to write a small API for flat modules, and whenever I want to use category theory (say, tensoring preserves (co)limits), then I need everything to be in the same universe.
It would be cool if we could just start a proof with ulift (max u v w) and from then on all types have been replaced by types that live in one big universe.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:01):

Do you have a real use case where more than one universe is necessary? I spent 30 years doing homological algebra in one universe.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:02):

But you used a really wonky definition of etale cohomology, just to stay inside that universe.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:02):

And then you deduced all sorts of nice results about it using topos machinery that doesn't actually work without a bigger universe.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:07):

Isn't the idea that you define the cohomology theory and it bumps the universe, and then you prove a theorem that it lives in the smaller universe because it can be calculated using some small limit?

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:07):

Right... there is your ulift

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:07):

Aha

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:07):

Every time you want to prove something about etale cohomology, you need to use that ulift.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:08):

Or just deal with it, and let it live in the bigger universe to begin with.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:08):

Right

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:08):

I guess this whole story might be easier with cumulative universes...

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:09):

@Mario Carneiro what is the downside of cumulative universes? Apart from ugly foundations?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:09):

You'd better get onto Leo quick, it's almost the end of summer

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:09):

Well, the foundations thing is actually an open question

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:10):

I don't currently know how to extend the proof that lean is consistent to the cumulative case

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:10):

It's probably possible, Coq has some literature on similar stuff, but the devil is in the details

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:10):

So one would end up with two etale cohomology functions, one of which bumps universe and one of which doesn't

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:11):

Right, and the one which doesn't is the one you can prove things about.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:11):

But it means that you now will have a module in Type 1 living over a ring in Type 0.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:11):

But people would instinctively use the non bumping one I guess, if available

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:11):

It sounds like kevin just wants to work in ZFC :P

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:12):

Why does that solve the issue?

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:12):

Because you don't have types to begin with, I guess

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:12):

well if you don't have universes that's essentially what you get

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:12):

If you don't have universes, then proving things about etale cohomology becomes a lot more painful.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:12):

Brian Conrad can do that. But he doesn't formalise it.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:13):

Right, you get de Jong's section in stacks where he explains how set theoretic foundations can be used to make sure etale cohomology groups are sets despite them being not obviously sets in ZFC

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:14):

But also all the topos machinery goes bad

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:14):

So I think I would rather have a ulift tactic

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:15):

What is the problem with just developing the API with the bumping definition and then deducing everything for the non bumping one after? Is this why you think we need the tactic?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:16):

One would need things like " if A and B are in universe u+1 and there's a map between them, and if A and B descend to u then so does the map"

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:17):

Is this true in DTT? it's certainly true in ZFC although one probably uses replacement

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:17):

It depends on what you mean by descend

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:17):

@Kevin Buzzard In lean that "descend" is going to look ugly.

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:18):

if you mean you have an equiv then yes, since you can just compose with the equiv

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:18):

Well, every finite-dimensional vector space over K : Type will descend from Type u to Type

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:19):

But it will be using choice.

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:19):

The equiv would be between Abig and ulift Asmall

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:19):

And if you have a map from Abig to Bbig can you get a map from Asmall to Bsmall?

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:20):

Sure, like Mario said, just compose with the equivs

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:20):

I don't get it

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:20):

equiv (and the linear variants) are universe polymorphic

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:20):

But iso (in category_theory) is not

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

What universe do the equivs live in?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

Oh I see

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:21):

max (small big)

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

So the maps will be in the wrong universe?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

I'm trying to descend the maps

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

I can't use equiv if the equiv is in the wrong universe

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:21):

Can I?

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:22):

Asmall -> Abig -> Bbig -> Bsmall

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:22):

that composition will be small, right?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:22):

I see!

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:22):

It uses bigger universes in its definition, but not in the type.

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:23):

And you won't get around using bigger universes in its definition, because that's what it's meant to do.

view this post on Zulip Mario Carneiro (Oct 15 2020 at 07:23):

which is why lean restricted to the first universe is still stronger than ZFC

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:23):

The descent of eg fdvs involves choice but this sounds right to me because a cohomology theory is a universal object so only defined up to isomorphism anyway

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:24):

doesn't mean that it will be nice to work with

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:24):

De Jong's treatment in ZFC involves some random choice of a sufficiently large cardinal

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:25):

So there's the choice there

view this post on Zulip Johan Commelin (Oct 15 2020 at 07:25):

Sure, but afterwards, he never has to mention it again

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:25):

It's like localisation isn't it?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:26):

One should use choice to prove the existence of the universal delta functor in the right universe

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:26):

But one should prove theorems about all universal delta functors

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:28):

Let H be a cohomology theory which satisfies the axioms of etale cohomology. Then...

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:29):

No choice involved there

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:29):

Will this run into issues though? We can only find out by trying, I should imagine

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:30):

Can the theory be developed in the generality where the cohomology groups live in a possibly different universe to the schemes?

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:32):

I'm giving a lean graduate course next term and was going to spend some time discussing algebraic geometry but I'm not sure we'll get as far as etale cohomology

view this post on Zulip Kevin Buzzard (Oct 15 2020 at 07:32):

In fact I'm sure we'll not

view this post on Zulip Gabriel Ebner (Oct 15 2020 at 08:12):

Johan Commelin said:

It would be cool if we could just start a proof with ulift (max u v w) and from then on all types have been replaced by types that live in one big universe.

How far do you get with equiv_rw? Is this just a matter of UI, or are we missing some more fundamental tools?

equiv_rw (semimodule_equiv.symm : M ≃ₗ[R] ulift.{(max u v w)} M) at M,

(Note: I've never used equiv_rw in practice, but this seems to be exactly what it's meant for.)

view this post on Zulip Johan Commelin (Oct 15 2020 at 08:48):

@Gabriel Ebner Oooh sweet. I guess that gets me pretty close!

view this post on Zulip Johan Commelin (Oct 15 2020 at 08:48):

For now that should be good enough


Last updated: May 11 2021 at 00:31 UTC