## Stream: maths

### Topic: category theory notations

#### Scott Morrison (Apr 28 2018 at 05:45):

I am very-nearly-just-about ready with my category theory PR. I would like some help with notations, however.

#### Scott Morrison (Apr 28 2018 at 05:46):

Perhaps I will write up a short document explaining my current choices, and hopefully some of the mathematicians (/computer scientists who like category theory) here can complain about them. :-)

#### Kenny Lau (Apr 28 2018 at 05:48):

@Scott Morrison fancy incorporating my examples?

#### Scott Morrison (Apr 28 2018 at 05:53):

@Kenny Lau which examples?

#### Scott Morrison (Apr 28 2018 at 05:53):

I'll look, but it may just be best to do a later PR.

#### Scott Morrison (Apr 28 2018 at 05:54):

My first category theory PR is going to be a tiny subset of the whole existing library.

#### Kenny Lau (Apr 28 2018 at 05:54):

@Kenny Lau which examples?

I have many examples in my repo :P

#### Kenny Lau (Apr 28 2018 at 05:54):

https://github.com/kckennylau/category-theory

#### Scott Morrison (Apr 28 2018 at 06:05):

okay --- let's wait until we have the basics in mathlib, and then we can start importing!

#### Reid Barton (Apr 28 2018 at 06:16):

@Scott Morrison, I should have mentioned this earlier, but I noticed that your Complete C class doesn't quite correspond to the usual notion of completeness, since one ordinarily only requires the indexing category J for a limit to be small (w.r.t. the same universe in which the hom sets of C are small), but your definition further requires the hom sets of J to belong to an even smaller universe.

#### Reid Barton (Apr 28 2018 at 06:17):

More concretely, in a complete category one may always form the equalizer of all the morphisms between a given pair of objects, but that's not possible with the Complete class.

#### Reid Barton (Apr 28 2018 at 06:21):

And generally speaking it is useful to have a notion of "small category" where the objects and morphisms are sets that live in the same universe. I mention this because one possible way to address this (though maybe not the best way) would be to add a second universe parameter to the category class, which would probably involve many other changes.

#### Reid Barton (Apr 28 2018 at 06:31):

Another option might be to define a small category as a category with object type of the form ulift.{i (i+1)} a

(deleted)

(deleted)

#### Kevin Buzzard (Apr 28 2018 at 11:41):

It seems to me that doing category theory in Lean brings up some extremely delicate issues.

#### Kevin Buzzard (Apr 28 2018 at 11:42):

I am an end user and I do not care about universes or these subtleties, at least when I have my algebraic geometry hat on

#### Kevin Buzzard (Apr 28 2018 at 11:42):

I just want to write down a functor from "the" category of open sets on a topological space to "the" category of groups, without caring at all about which universe all these things live in.

#### Kevin Buzzard (Apr 28 2018 at 11:44):

On the other hand, I have seen intelligent people occasionally pausing to say "by the way, when I say category of _all_ schemes, it might be best if you interpret this as the category of all schemes which show up at some level in a set-theoretical hierarchy, and here is a calculation indicating that certain basic operations will never take us out of that category"

#### Kevin Buzzard (Apr 28 2018 at 11:46):

Here, for example, is Johan de Jong being very careful about what he means by the category of schemes, as formalised within ZFC.

#### Kevin Buzzard (Apr 28 2018 at 11:46):

https://stacks.math.columbia.edu/tag/000H

#### Kevin Buzzard (Apr 28 2018 at 11:47):

It seems to me that when you are doing calculations such as these, you are making a promise to your reader.

#### Kevin Buzzard (Apr 28 2018 at 11:48):

You are saying "isn't maths great, look at all the things we can do. Here is one thing we can do which is quite sensible -- we can sometimes take certain limits of schemes. And look, if my schemes are all "small" and the diagram is "small" then the limit of the diagram is "small" too."

#### Kevin Buzzard (Apr 28 2018 at 11:49):

And now you make the promise that throughout the 6000 pages which are about to follow

#### Kevin Buzzard (Apr 28 2018 at 11:49):

you promise you don't do anything pathological

#### Kevin Buzzard (Apr 28 2018 at 11:49):

which forces a universe change

#### Kevin Buzzard (Apr 28 2018 at 11:49):

Now that is a really big promise.

#### Kevin Buzzard (Apr 28 2018 at 11:50):

But some mathematicians are absolutely alive to that promise.

#### Kevin Buzzard (Apr 28 2018 at 11:50):

and it's those kinds of mathematicians, like Brian Conrad, who, when you mention the fpqc topology on a scheme, points out that in that situation you have not kept your promise.

#### Kevin Buzzard (Apr 28 2018 at 11:50):

because an arbitrary map between fields is quasi-compact

#### Kevin Buzzard (Apr 28 2018 at 11:51):

and there are a lot of fields

#### Kevin Buzzard (Apr 28 2018 at 11:51):

What I am pretty convinced about is that one day in the future when we have formalised schemes, and their etale cohomology, their fppf cohomology and their fpqc cohomology

#### Kevin Buzzard (Apr 28 2018 at 11:52):

then at some point there will be an issue with fpqc

#### Kevin Buzzard (Apr 28 2018 at 11:52):

which will manifest itself in some constructions having to be worked out slightly differently

#### Kevin Buzzard (Apr 28 2018 at 11:52):

because of universe issues

#### Kevin Buzzard (Apr 28 2018 at 11:52):

I believe that mathematicians hide that thought away

#### Kevin Buzzard (Apr 28 2018 at 11:53):

because it hopefully doesn't affect anything they do

#### Kevin Buzzard (Apr 28 2018 at 11:54):

Scott -- if you could just give me some working definition of a category and a site and a topos

#### Kevin Buzzard (Apr 28 2018 at 11:54):

then there is nothing stopping people from formalising definitions of these fancy cohomology theories in Lean

#### Kevin Buzzard (Apr 28 2018 at 11:54):

Proving anything non-trivial about these fancy cohomology theories would almost certainly be extemely difficult

#### Kevin Buzzard (Apr 28 2018 at 11:54):

however _defining_ them is another kettle of fish

#### Kevin Buzzard (Apr 28 2018 at 11:55):

I defined schemes over a month ago and am still yet to produce a single example because I have been caught up in notions of canonical isomorphism

#### Kevin Buzzard (Apr 28 2018 at 11:55):

but the definition is there

#### Kevin Buzzard (Apr 28 2018 at 11:55):

So let me know when you want to define some fancy cohomology theories on the category of schemes

#### Kevin Buzzard (Apr 28 2018 at 11:56):

and not prove anything about them

#### Kevin Buzzard (Apr 28 2018 at 11:56):

because this would be an extremely good stress test for your category theory library

#### Kevin Buzzard (Apr 28 2018 at 11:56):

and I believe it is within reach

Last updated: May 19 2021 at 00:40 UTC