Zulip Chat Archive

Stream: maths

Topic: Categories and Universes in Lean


Lambert A'Campo (Dec 08 2019 at 14:50):

Can someone explain what (K : Type u) [category.{v} K] means mathematically? Here is my attempt at translating it into mathematics based on set theory: First of all, u and v are universes in this sense https://en.wikipedia.org/wiki/Grothendieck_universe, then K is a category whose objects are elements of u and whose morphisms are elements of v.

But if this is correct, then how is the category of all sets modeled in lean?

Reid Barton (Dec 08 2019 at 15:11):

No, the set of objects of K is an element of u and for each pair of objects X and Y, the set Hom(X, Y) is an element of v.

Lambert A'Campo (Dec 08 2019 at 15:32):

ok, so that means Sets is not a category in lean ?

Reid Barton (Dec 08 2019 at 15:34):

It is a category

Reid Barton (Dec 08 2019 at 15:34):

called Type v

Lambert A'Campo (Dec 08 2019 at 15:35):

but there is no set of objects of Sets

Reid Barton (Dec 08 2019 at 15:35):

Well, I'm assuming "Set" means the category of sets which are elements of some fixed reference universe v

Reid Barton (Dec 08 2019 at 15:36):

its set of objects is v itself, which is an element of some bigger universe v+1

Lambert A'Campo (Dec 08 2019 at 15:37):

Yes ok I'm just surprised there is no notion of category of sets without mentioning any universe. But maybe that is just an unnatural thing in type theory.

Reid Barton (Dec 08 2019 at 15:38):

To be honest, it's not a very good notion in ordinary math, either

Kenny Lau (Dec 08 2019 at 15:38):

Yes ok I'm just surprised there is no notion of category of sets without mentioning any universe. But maybe that is just an unnatural thing in type theory.

yeah that doesn't exist

Kenny Lau (Dec 08 2019 at 15:38):

everything has a universe

Lambert A'Campo (Dec 08 2019 at 15:41):

To be honest, it's not a very good notion in ordinary math, either

fair enough

Kevin Buzzard (Dec 08 2019 at 15:58):

In ZFC people would talk about the "category of sets" -- for them, the objects are what ZFCists would call a class, and Hom(X,Y) is a set for all X and Y.

Kevin Buzzard (Dec 08 2019 at 16:01):

Grothendieck was precise in SGA4 but introduced universes. Some ZFC people don't like that (because the existence of a universe implies the existence of a set satisfying the axioms of ZFC, which implies ZFC is consistent, so by Goedel we deduce that we cannot prove the existence of universes in ZFC). People like de Jong have written down in the Stacks project the way that ZFC people can carefully get around issues such as cohomology of a sheaf on the etale site being defined as a limit over a class. Other mathematicians simply don't care about these issues. My belief is that these other mathematicians are secretly using different foundations, because they think that all this kappa-cutoff stuff is boring and regard it as a deficiency of ZFC foundations. Grothendieck thought like this. He wanted to do mathematics, and if ZFC didn't let him do the mathematics he wanted then he was just going to do it anyway and in his mind this said more about ZFC than the theory of sheaves on a site.

Kevin Buzzard (Dec 08 2019 at 16:12):

To do etale cohomology you need etale sheaves. To do etale sheaves you need to know about sheafification on sites (not just on top spaces like we needed in the schemes project). Here is sheafification in the stacks project (you can trace back to this page from the etale cohomology pages). In example 7.10.2 we discover that in the stacks project, the objects of a category form a set, so the limits are not problematic but we deduce that it must be the categories which are problematic, because the objects in the category of schemes for sure do not form a set. De Jong gives a very precise definition of site here and then he remarks that this differs from the SGA4 definition. This is a great example of mathematicians meaning different things by the same words, and because the details here are technical and boring and "not mathematics" or "not proper mathematics", we just claim that the logicians sorted all this out ages ago, even though I am not sure how many logicians are reading SGA4. I do know some who have looked at this. However I don't know any who are looking at Scholze's work which needs infinity categories and all the same questions are there.

Reid Barton (Dec 08 2019 at 16:14):

There are already more basic issues. Take a theorem of category theory like "a right adjoint functor preserves limits". Actually, in ZFC, it cannot be a theorem, unless you restrict to small categories, in which case you exclude most cases of interest.

Kevin Buzzard (Dec 08 2019 at 16:16):

On the other hand, I am confident that these tedious foundational issues have or can all be resolved, and it's just a case of resolving them. My instinct is to just say "screw ZFC, we're working in dependent type theory with universes so let's use them when we need them, and now looks like a good time". If we are challenged later on by people who say our sheafification procedure doesn't work in ZFC then we can tell them to do it all in Mizar or whatever.

Kevin Buzzard (Dec 08 2019 at 16:18):

I still don't know the definition of a site though. In Wikipedia it uses this word "collection" when defining a Grothendieck topology (see 5th paragraph). What does that word mean? Is it a 3rd universe w?

Reid Barton (Dec 08 2019 at 16:20):

Actually I think, to the extent anyone really cares at all, this is a very good application of formalization, because I would much rather trust some automated procedure which determines whether universes can be eliminated from a proof (say of FLT) than trust a human, who probably doesn't understand both the relevant logic and the proof in question.

Kevin Buzzard (Dec 08 2019 at 16:24):

You're talking like a crank Reid, every proper mathematician knows that the proof of FLT doesn't use universes ;-) I read it on the internet!

Kevin Buzzard (Dec 08 2019 at 16:27):

https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof There, Brian Conrad says it's fine so stop worrying

Kevin Buzzard (Dec 08 2019 at 17:57):

To get back to the point (and to remove my tongue from my cheek), @Calle Sönne wants to define sites in Lean and there is a universe question. The objects of a category in Lean are something to do with a universe u. The morphisms are something to do with a universe v. For a site we also need the coverings. Are they something to do with u? With v? With a new universe w? Or should we mathematicians simply be sticking with Type at this point and not bothering with these questions?

Kevin Buzzard (Dec 08 2019 at 17:57):

@Bhavik Mehta you have experience with elephants, right?

Bhavik Mehta (Dec 08 2019 at 17:58):

Some experience, yeah

Kevin Buzzard (Dec 08 2019 at 18:02):

So is the big etale site a site according to PTJ?

Kevin Buzzard (Dec 08 2019 at 18:04):

Option 1: we stick to schemes S : C where C : Type 1, check Hom(X,Y) : Type, and demand that a cover of S is Cov(S) : Type. This will involve some jiggery-pokery with cardinals.

Kevin Buzzard (Dec 08 2019 at 18:04):

Option 2: S : C, C : Type 1, Hom(X,Y) : Type, but Cov(S) : Type 1. @Reid Barton can you check my working? With this option no cardinals are necessary.

Kevin Buzzard (Dec 08 2019 at 18:05):

Option 3: full ZFC. Choose a sufficiently large cardinal, remark that one might occasionally have to increase it. Now S : C, C : Type (not Type 1 any more) and everything is in Type basically, because Type is all we believe in.

Kevin Buzzard (Dec 08 2019 at 18:07):

Option 4: fully universe polymorphic. C : Type u, Hom(S,T) : Type v, and Cov(S) : Type w. Is this a site? I could envisage the type theorists among us here arguing that this is clearly the correct definition as far as Lean is concerned.

@Johan Commelin which one did you use when you did sites?

Johan Commelin (Dec 08 2019 at 18:09):

I think for me w was equal to u or max u v. I moved back an forth between different things a bit.

Edward Ayers (Dec 08 2019 at 18:23):

I've been helicoptered in by Bhavik, I had a go at implementing sites a while ago for fun. I implemented them as:

def slice (C : Type u) [category.{v} C] (X : C) := Σ Y, Y  X

structure sieve (X : C) :=
(arrows : set (slice C X))
(subs : Π (f : slice C X) (_ : f  arrows) (Z : C) (g : Z  f.1), (slice.mk (g  f.2))  arrows)

def sieve_set (C : Type u) [𝒞 : category.{v} C] :=  Π (X : C), set (@sieve C 𝒞 X)

structure Site :=
(C : Type u)
[𝒞 : category.{v} C]
(J : sieve_set C)
[g : @grothendieck C 𝒞 J]

So I think if you can express your category by choosing u and v properly, you can define sites on it and I didn't have any universe problems there. Although I didn't get as far as defining the Etale site.

Edward Ayers (Dec 08 2019 at 18:35):

I would also like to say that I don't understand sites and schemes and stuff and this was more of a personal learning exercise.


Last updated: Dec 20 2023 at 11:08 UTC