Zulip Chat Archive

Stream: maths

Topic: category theory notations


view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:48):

@Scott Morrison fancy incorporating my examples?

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:53):

@Kenny Lau which examples?

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:53):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:54):

@Kenny Lau which examples?

I have many examples in my repo :P

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:54):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 28 2018 at 07:10):

(deleted)

view this post on Zulip Scott Morrison (Apr 28 2018 at 07:10):

(deleted)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:46):

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

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:49):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:49):

you promise you don't do anything pathological

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:49):

which forces a universe change

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:49):

Now that is a really big promise.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:50):

But some mathematicians are absolutely alive to that promise.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:50):

because an arbitrary map between fields is quasi-compact

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:51):

and there are a lot of fields

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:52):

then at some point there will be an issue with fpqc

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:52):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:52):

because of universe issues

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:52):

I believe that mathematicians hide that thought away

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:53):

because it hopefully doesn't affect anything they do

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:54):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:54):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:54):

however _defining_ them is another kettle of fish

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:55):

but the definition is there

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:56):

and not prove anything about them

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:56):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 11:56):

and I believe it is within reach


Last updated: May 19 2021 at 00:40 UTC