Zulip Chat Archive

Stream: general

Topic: avoiding universe issues


view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:41):

I was about to jump in with the following definitions:

structure presheaf_of_complete_topological_rings (X : Type u) [T : topological_space X] :=
(F : Π {U : set X}, T.is_open U  Type v) -- note v
[some more stuff]

structure preadic_space -- a category
(X : Type u)
(F : presheaf_of_complete_topological_rings X)
[loads more stuff]

But both of these definitions are "bad", right? In the sense that Mario told me to expect universe problems with structures like this, where I introduce new universes in structure fields.

So I looked back at my schemes definition and indeed I have

structure presheaf_of_types (α : Type u) [T : topological_space α] :=
(F : Π {U : set α}, T.is_open U  Type u) -- note u
...

but I do also have

structure scheme :=
(α : Type u)
(T : topological_space α)
(O_X : presheaf_of_rings α)
...

Is this then a "bad" definition of scheme? Should it be scheme α?

And is this why category theory is difficult? This is what causes universe problems?

Should one really define the category of schemes in a universe u?

I don't really understand why introducing new universe variables in fields is a bad idea. Is it sometimes Ok to do it?

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:42):

Here's a better question. If I can avoid the pre-adic space definition above, and instead do preadic_space X, is that preferable? [and if so, why?]

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:45):

If you use a structure with an "internal" universe variable like this, you should expect to need to specify that universe as in presheaf_of_complete_topological_rings.{u v}. This is what happens with category

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:45):

As for whether it's required, that depends on your application

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:49):

I have a lot of difficulty with category theory in part because it's so heavy on definitions and light on applications. I use the applications to judge the definitions

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:52):

What will happen when someone wants to do stacks and we need 2-categories to formalise the definition?

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:53):

I guess we get 2-categories

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:53):

But will there be new kinds of problems?

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:53):

yes

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:53):

cool

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 20:53):

something to look forward to

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:53):

the biggest one is probably that we will have to do all of category theory again

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:54):

and there really isn't a good way to unify these

view this post on Zulip Mario Carneiro (Mar 09 2019 at 20:55):

Probably it's best to just do this stuff on a by-need basis because there's no end of generalization


Last updated: May 08 2021 at 09:11 UTC