Zulip Chat Archive

Stream: general

Topic: automation to fix universe issues


Kevin Buzzard (Dec 09 2019 at 18:41):

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 (Dec 09 2019 at 19:08):

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 (Dec 09 2019 at 19:51):

I thought this was the algorithm

Mario Carneiro (Dec 09 2019 at 19:52):

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

Mario Carneiro (Dec 09 2019 at 19:53):

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 (Dec 09 2019 at 19:56):

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 (Dec 09 2019 at 19:57):

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 (Dec 09 2019 at 20:06):

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 (Dec 10 2019 at 15:01):

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 (Dec 10 2019 at 15:01):

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

Kevin Buzzard (Dec 10 2019 at 15:02):

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 (Dec 10 2019 at 15:06):

@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 i0H0(X,ωXi)\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 (Dec 10 2019 at 15:06):

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

Johan Commelin (Dec 10 2019 at 15:07):

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

Kevin Buzzard (Dec 10 2019 at 15:08):

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 (Dec 10 2019 at 15:08):

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 (Dec 10 2019 at 15:11):

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 (Dec 10 2019 at 15:33):

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 (Dec 10 2019 at 15:50):

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 i0H0(X,ωXi)\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 (Dec 10 2019 at 15:53):

Ha, that might be an example.

Johan Commelin (Dec 10 2019 at 15:53):

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

Johan Commelin (Dec 10 2019 at 15:55):

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

Kevin Buzzard (Dec 11 2019 at 00:59):

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

Kevin Buzzard (Dec 11 2019 at 01:03):

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 (Dec 11 2019 at 01:04):

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 (Dec 12 2019 at 09:54):

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 (Dec 12 2019 at 09:59):

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 (Dec 12 2019 at 10:45):

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


Last updated: Dec 20 2023 at 11:08 UTC