## Stream: general

### Topic: avoiding universe issues

#### 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)


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?

#### 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?]

#### 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

#### Mario Carneiro (Mar 09 2019 at 20:45):

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

#### 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

#### 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?

#### Mario Carneiro (Mar 09 2019 at 20:53):

I guess we get 2-categories

#### Kevin Buzzard (Mar 09 2019 at 20:53):

But will there be new kinds of problems?

yes

cool

#### Kevin Buzzard (Mar 09 2019 at 20:53):

something to look forward to

#### Mario Carneiro (Mar 09 2019 at 20:53):

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

#### Mario Carneiro (Mar 09 2019 at 20:54):

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

#### 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