automation to fix universe issues

Stream: general

[Kevin Buzzard]

As we move on through mathematics we're running into interesting questions about universes. Scott Morrison has set up the category theory library so objects are in universe u and morphisms in universe v, and there are good mathematical reasons to keep the universes separate. This has annoying consequences, which Scott has done his best to work around in Lean 3, but one still has to sometimes write blah.{v} instead of blah just to help Lean on its way with unification.

Having talked to several other mathematicians about universes really, it has become pretty clear that everyone knows there's some sort of an issue with the set of all sets, but they really don't care about universes.

I think that what would make mathematicians happy would be the following interface: we just put Type * or Sort * for everything, we let Lean be as polymorphic as possible, we can put blah.{*} or just even blah and tell Lean to do the sensible thing, and at the end of the day if we ever work out the cohomology of the real numbers and it turns out that it is the trivial group in type Type 3 because three times in our argument we took a limit over a thing that wasn't a set, then we don't care but make a mental note that the ZFC people might want to add something here. Is this algorithm going to be available in Lean 4?

[Kevin Buzzard]

Then the idea could be that the logicians can just slot in extra stuff into the algorithm if they think they can save a universe

[Mario Carneiro]

I thought this was the algorithm

[Mario Carneiro]

if by "the sensible thing" you mean inventing a new universe variable for every unresolved metavariable

[Mario Carneiro]

Although, that doesn't always work, for instance you might have to solve the universe equation max 2 ? = 2 and the answer isn't uniquely determined (but putting a variable in there wouldn't work)

[Mario Carneiro]

You should keep in mind that universe handling is already incredibly rare, so the lean elaborator seems to be working to keep it out of your hair most of the time, like when you just have a bunch of functions to apply. It's only when you actually use universes in a non-default way that they start showing up

[Mario Carneiro]

Having talked to several other mathematicians about universes really, it has become pretty clear that everyone knows there's some sort of an issue with the set of all sets, but they really don't care about universes.

This doesn't give me the least bit of confidence. This is exactly the sort of situation where I expect a theorem prover to get pedantic on me

[Mario Carneiro]

I'm convinced that category theory is the refuge of people that want to recover the glory days of Frege before Russell's paradox knocked everything down. "Sure there's a paradox, but it doesn't apply to me, because, mumble mumble kappa-accessible..."

[Kevin Buzzard]

I'm less convinced of this. Freek Wiedijk told me earlier this year that his favourite type theory for getting things done was Type-In-Type. When I remarked that this was inconsistent he said that he didn't care because he wasn't going to do anything stupid. I think that this is a very mathematical attitude. Having to write blah.{v} is a bit annoying, I want Lean to make liberal decisions, unify everything, and if it turns out that some cohomology theories live in a different universe to the one mathematicians think they live in because they neglected some subtlety about limits commuting with universes then I wonder whether this really even matters.

[Kevin Buzzard]

i.e. "Sure there's a paradox, but it doesn't apply to me, because, mumble mumble kappa-accessible..."

[Kevin Buzzard]

a.k.a section 4 of https://arxiv.org/abs/1709.07343, and this chapter of the stacks project. We've got it covered.

[Johan Commelin]

@Kevin Buzzard Do you know of a construction where you start with some geometric thingy, say a scheme, then you take some cohomology ring (maybe it's graded, like $\bigoplus_{i \ge 0} H^0(X, \omega_X^{\otimes i})$) and then you take Spec or Proj of that. This gives you another scheme. And now maybe there is a some reason you want to iterate this construction, and maybe take a limit over the iterations?

[Johan Commelin]

I don't know exactly of such a construction, but I could imagine it exists.

[Johan Commelin]

That graded ring in my example shows up in the Kodaira dimension. But you don't really iterate it.

[Kevin Buzzard]

The way I read section 4 of Scholze is this: "We choose a large cardinal whose existence can prove in ZFC. We then create a "pseudouniverse" of stuff of "size at most kappa". This is not closed under all universe stuff, but it is closed under the stuff we want, and the answers it spits out when we take limits are "equal" to the answers we're going to get if we just don't introduce kappa at all, however they do live one universe closer to the bottom". I don't see why Scholze should be wasting his time writing these sections, these can be done independently by people who just want to fiddle with some universe framework. Scholze is making a claim that he never does anything "mathematically unreasonable" in the 120 pages that follow section 4, and the arguments in there do not really fit in the paper, they should just be set-theoretical asides which are hidden from mathematicians.

[Johan Commelin]

Anyway, if such a construction bumps your universe, then you can only iterate it explicitly in Lean (so you can't parameterize the iterations by ℕ) and in particular you can't take the limit

[Kevin Buzzard]

The construction you're outlining Johan isn't problematic at all as far as I can see. The new ring lives in the same universe as the old, and if you only take a countable limit or more generally a limit over a set then there are also no set-theoretic problems. The issue comes when computing Cech cohomology by taking a limit over all covers. Then there are tricks to deal with the universe problems in ZFC, but it is not so clear to me that these tricks deserve to be called mathematics, they seem to me to be completely ZFC-specific. I am now wondering whether, if I'm deciding to work in Lean, I should just adopt Lean's type theory and ask the computer scientists nicely to make all the universes go away and then not worry any more, and the ZFC people can worry instead.

[Johan Commelin]

If X : Scheme.{u} then bigplus H(X, omega^i) : Type (u+1) for mathematical definitions of cohomology. Hence the new scheme lives in Scheme.{u+1}.

[Alex J. Best]

Kevin Buzzard Do you know of a construction where you start with some geometric thingy, say a scheme, then you take some cohomology ring (maybe it's graded, like $\bigoplus_{i \ge 0} H^0(X, \omega_X^{\otimes i})$) and then you take Spec or Proj of that. This gives you another scheme. And now maybe there is a some reason you want to iterate this construction, and maybe take a limit over the iterations?

Does an infinite sequence of blow ups meet your criteria perhaps? I've definitely seen that happen in a couple of places.

[Johan Commelin]

Ha, that might be an example.

[Johan Commelin]

But does the "mathematical" definition of blow-up bump universes?

[Johan Commelin]

I think https://en.wikipedia.org/wiki/Blowing_up#Blowing_up_schemes looks fine. This shouldn't bump universes

[Kevin Buzzard]

Oh I see, it's the cohomology which is bumping the universe, not the limit

[Kevin Buzzard]

If this is just sheaf cohomology then that won't bump up the limit because the diagram category is small. The issue comes with etale cohomology. I have no doubt that this sort of stuff has been studied to death but I don't know of any reference which uses type theory. Johan's point is I guess that ignoring universes completely can in theory be bad if you do infinitely many bumps up of the universe. So IF YOU WANT TO TAKE THAT LIMIT (and as far as we know you don't) then you need to get a ZFC person in who will start analysing your objects and checking that they're small enough. This just seems to be like a question which one can abstract away from the mathematics

[Kevin Buzzard]

And I'm not convinced we ever want to take that limit. I have seen infinitely many blowups before, you can get valuations on 2d function fields this way, but the problem is not the infinity, it's the cohomology

[David Michael Roberts]

Here's a case where a category theorist took the care to figure out something like you mention of Scholze's ch 4: https://arxiv.org/abs/1304.5227

[David Michael Roberts]

Unfortunately, as soon as one allows the possibility of changing U, one also has to face the fact that universal constructions such as limits or adjoints or Kan extensions could, in principle, depend on the parameter U. We will prove this is not the case for adjoints of accessible functors between locally presentable categories (and hence, limits and Kan extensions), making explicit the idea that "bounded" constructions do not depend on the choice of U.

[Kevin Buzzard]

Right, this is exactly the sort of which which is going on. Scholze in his Bonn lecture notes comes up with cardinals which aren't universes and again shows that everything he does is independent of the choice. I feel like these things should be demoted to out of the way