Stream: general

Topic: ulift tactic

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.

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.

Johan Commelin (Oct 15 2020 at 07:02):

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

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.

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?

Johan Commelin (Oct 15 2020 at 07:07):

Right... there is your ulift

Aha

Johan Commelin (Oct 15 2020 at 07:07):

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

Johan Commelin (Oct 15 2020 at 07:08):

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

Right

Johan Commelin (Oct 15 2020 at 07:08):

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

Johan Commelin (Oct 15 2020 at 07:09):

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

Kevin Buzzard (Oct 15 2020 at 07:09):

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

Mario Carneiro (Oct 15 2020 at 07:09):

Well, the foundations thing is actually an open question

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

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

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

Johan Commelin (Oct 15 2020 at 07:11):

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

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.

Kevin Buzzard (Oct 15 2020 at 07:11):

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

Mario Carneiro (Oct 15 2020 at 07:11):

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

Johan Commelin (Oct 15 2020 at 07:12):

Why does that solve the issue?

Johan Commelin (Oct 15 2020 at 07:12):

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

Mario Carneiro (Oct 15 2020 at 07:12):

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

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.

Johan Commelin (Oct 15 2020 at 07:12):

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

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

Johan Commelin (Oct 15 2020 at 07:14):

But also all the topos machinery goes bad

Johan Commelin (Oct 15 2020 at 07:14):

So I think I would rather have a ulift tactic

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?

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"

Kevin Buzzard (Oct 15 2020 at 07:17):

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

Mario Carneiro (Oct 15 2020 at 07:17):

It depends on what you mean by descend

Johan Commelin (Oct 15 2020 at 07:17):

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

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

Johan Commelin (Oct 15 2020 at 07:18):

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

Johan Commelin (Oct 15 2020 at 07:19):

But it will be using choice.

Kevin Buzzard (Oct 15 2020 at 07:19):

The equiv would be between Abig and ulift Asmall

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?

Johan Commelin (Oct 15 2020 at 07:20):

Sure, like Mario said, just compose with the equivs

I don't get it

Johan Commelin (Oct 15 2020 at 07:20):

equiv (and the linear variants) are universe polymorphic

Johan Commelin (Oct 15 2020 at 07:20):

But iso (in category_theory) is not

Kevin Buzzard (Oct 15 2020 at 07:21):

What universe do the equivs live in?

Oh I see

Johan Commelin (Oct 15 2020 at 07:21):

max (small big)

Kevin Buzzard (Oct 15 2020 at 07:21):

So the maps will be in the wrong universe?

Kevin Buzzard (Oct 15 2020 at 07:21):

I'm trying to descend the maps

Kevin Buzzard (Oct 15 2020 at 07:21):

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

Can I?

Johan Commelin (Oct 15 2020 at 07:22):

Asmall -> Abig -> Bbig -> Bsmall

Johan Commelin (Oct 15 2020 at 07:22):

that composition will be small, right?

I see!

Johan Commelin (Oct 15 2020 at 07:22):

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

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.

Mario Carneiro (Oct 15 2020 at 07:23):

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

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

Johan Commelin (Oct 15 2020 at 07:24):

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

Kevin Buzzard (Oct 15 2020 at 07:24):

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

Kevin Buzzard (Oct 15 2020 at 07:25):

So there's the choice there

Johan Commelin (Oct 15 2020 at 07:25):

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

Kevin Buzzard (Oct 15 2020 at 07:25):

It's like localisation isn't it?

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

Kevin Buzzard (Oct 15 2020 at 07:26):

But one should prove theorems about all universal delta functors

Kevin Buzzard (Oct 15 2020 at 07:28):

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

Kevin Buzzard (Oct 15 2020 at 07:29):

No choice involved there

Kevin Buzzard (Oct 15 2020 at 07:29):

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

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?

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

Kevin Buzzard (Oct 15 2020 at 07:32):

In fact I'm sure we'll not

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.)

Johan Commelin (Oct 15 2020 at 08:48):

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

Johan Commelin (Oct 15 2020 at 08:48):

For now that should be good enough

Last updated: Dec 20 2023 at 11:08 UTC