Zulip Chat Archive

Stream: general

Topic: How many universes did I use?


view this post on Zulip Kevin Buzzard (May 24 2018 at 19:49):

I proved a theorem in Lean (that an affine scheme is a scheme). Along the way I understood a little more about universes. In particular, I realised that the ZFC proof I knew that an affine scheme was a scheme "took place entirely within Type", by which I mean that every term I used was "good" -- here "good" is defined thus: (1) Type is good; (2) If X is a term of type Y and Y is good then X is good; (3) that's it. Once I realised this I went through a lot of files in my project that had lines of the form "universes u v w" and replaced them with "universe u", I also replaced many "Type v" and "Type *" with "Type u".

view this post on Zulip Kevin Buzzard (May 24 2018 at 19:49):

How do I check that I caught all of them?

view this post on Zulip Patrick Massot (May 24 2018 at 19:50):

What do you gain from these modifications?

view this post on Zulip Mario Carneiro (May 24 2018 at 19:56):

Agreed - these modifications do nothing toward your goal of eliminating unverse use

view this post on Zulip Mario Carneiro (May 24 2018 at 19:57):

What would help is using Type instead of Type u or Type*, but I don't recommend this

view this post on Zulip Chris Hughes (May 24 2018 at 19:57):

Doesn't changing Type v to Type u just make the theorem less general, and just worse?

view this post on Zulip Mario Carneiro (May 24 2018 at 19:58):

But your definition good is overly restrictive - ring is not good, not even ring.{0}, so ring A is also not good

view this post on Zulip Mario Carneiro (May 24 2018 at 19:59):

In fact clearly delineating what parts of DTT make sense in ZFC is rather delicate

view this post on Zulip Patrick Massot (May 24 2018 at 19:59):

We should have asked how many questions he marked before answering this thread

view this post on Zulip Kevin Buzzard (May 25 2018 at 09:59):

You're right that my definition of good is bad. I definitely don't want to put everything into Type because then other people won't want to use my code. But there is an underlying question here, and perhaps the answer is in Mario's comment "In fact clearly delineating what parts of DTT make sense in ZFC is rather delicate". I want to know the answer though. Is there any way I can find out whether my definition "would go through if I went through every file I used and removed all mention of universes, and changed all Type u and Type* to Type"?

view this post on Zulip Chris Hughes (May 25 2018 at 10:01):

It would go through, but nobody would be able to define a scheme structure on anything outside Type if I understand the question. So it would just be a less general definition.

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:02):

"It would go through" -- how do you know this?

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:02):

Cardinals wouldn't, right?

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:02):

I agree that it would be a bad idea to do so

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:03):

however I know people who care about this question.

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:03):

People whose _definition_ of mathematics is ZFC could argue that I am not doing mathematics if I use two universes.

view this post on Zulip Mario Carneiro (May 25 2018 at 10:03):

I've attempted to do this in my lean type theory paper

view this post on Zulip Chris Hughes (May 25 2018 at 10:03):

I misunderstood the question.

view this post on Zulip Mario Carneiro (May 25 2018 at 10:03):

several natural definitions were tried and dismissed

view this post on Zulip Kevin Buzzard (May 25 2018 at 10:04):

There are parts of mathlib which really use more than one universe, right?

view this post on Zulip Mario Carneiro (May 25 2018 at 10:04):

All parts of mathlib are universe polymorphic, so it's often hard to say, the answer is "yes trivially" if you don't ask carefully


Last updated: May 13 2021 at 18:26 UTC