# Zulip Chat Archive

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

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

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

yes

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

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: Aug 03 2023 at 10:10 UTC