ulift tactic

Stream: general

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

Right... there is your ulift

[Kevin Buzzard]

Aha

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

Right

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Well, the foundations thing is actually an open question

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Johan Commelin]

Why does that solve the issue?

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

But also all the topos machinery goes bad

[Johan Commelin]

So I think I would rather have a ulift tactic

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

It depends on what you mean by descend

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

But it will be using choice.

[Kevin Buzzard]

The equiv would be between Abig and ulift Asmall

[Kevin Buzzard]

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

[Johan Commelin]

Sure, like Mario said, just compose with the equivs

[Kevin Buzzard]

I don't get it

[Johan Commelin]

equiv (and the linear variants) are universe polymorphic

[Johan Commelin]

But iso (in category_theory) is not

[Kevin Buzzard]

What universe do the equivs live in?

[Kevin Buzzard]

Oh I see

[Johan Commelin]

max (small big)

[Kevin Buzzard]

So the maps will be in the wrong universe?

[Kevin Buzzard]

I'm trying to descend the maps

[Kevin Buzzard]

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

[Kevin Buzzard]

Can I?

[Johan Commelin]

Asmall -> Abig -> Bbig -> Bsmall

[Johan Commelin]

that composition will be small, right?

[Kevin Buzzard]

I see!

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

So there's the choice there

[Johan Commelin]

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

[Kevin Buzzard]

It's like localisation isn't it?

[Kevin Buzzard]

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

[Kevin Buzzard]

But one should prove theorems about all universal delta functors

[Kevin Buzzard]

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

[Kevin Buzzard]

No choice involved there

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

In fact I'm sure we'll not

[Gabriel Ebner]

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]

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

[Johan Commelin]

For now that should be good enough