Categories and Universes in Lean

Stream: maths

[Lambert A'Campo]

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]

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]

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

[Reid Barton]

It is a category

[Reid Barton]

called Type v

[Lambert A'Campo]

but there is no set of objects of Sets

[Reid Barton]

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

[Reid Barton]

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

[Lambert A'Campo]

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]

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

[Kenny Lau]

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]

everything has a universe

[Lambert A'Campo]

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

fair enough

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

@Bhavik Mehta you have experience with elephants, right?

[Bhavik Mehta]

Some experience, yeah

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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.