avoiding universe issues

Stream: general

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

I guess we get 2-categories

[Kevin Buzzard]

But will there be new kinds of problems?

[Mario Carneiro]

yes

[Kevin Buzzard]

cool

[Kevin Buzzard]

something to look forward to

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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