Stream: math-comp users

Topic: Developing basic (modern) algebraic geometry in mathcomp


view this post on Zulip Xuanrui Qi (Sep 16 2020 at 02:50):

I've recently started a development in MathComp of basic notions of modern (i.e., Grothendieck-style) algebraic geometry. My initial goal would be to define the notion of a scheme, and to do that I would first need to develop the notion of a sheaf. (BTW, I'm doing it in the classical way.) I'm using mathcomp-analysis for the classical set theory and topology and mathcomp-algebra for the basic ring theory part.

I wonder if there would be any interest from other MathComp users. As there are so many ways to do things (e.g., category theory), sometimes I wonder what is the "morally right" way to formalize notions like e.g. opposite categories.

view this post on Zulip Cyril Cohen (Sep 16 2020 at 19:19):

Hi @Xuanrui Qi that's great. I guess categories should be formalized using packedclasses

view this post on Zulip Bas Spitters (Sep 16 2020 at 20:18):

Category theory has been done many times in Coq, but not in MC yet, I believe
https://coq.discourse.group/t/survey-of-category-theory-in-coq/371

view this post on Zulip Enrico Tassi (Sep 17 2020 at 07:54):

Maybe it is the occasion for adding universe polymorphism to Elpi and Hierarchy Builder?

view this post on Zulip Xuanrui Qi (Sep 17 2020 at 12:33):

@Cyril Cohen That's indeed what I'm using now. I currently have a very basic hierarchy only (category -> productCategory; functor -> presheaf -> sheaf). But I want to define the notion of topos someday and that will indeed include a fairly complicated hierarchy.

view this post on Zulip Cyril Cohen (Sep 17 2020 at 12:43):

@Xuanrui Qi as @Enrico Tassi mentions, it may be useful to build it using Hierachy Builder when we fully support universe polymorphism (do you have an idea how long it would take Enrico?)

view this post on Zulip Xuanrui Qi (Sep 17 2020 at 12:45):

I currently don't have any universe polymorphism now, but I would soon need it (e.g., to define the category Cat of Type-small categories, and the categories PSh and Sh)

view this post on Zulip Enrico Tassi (Sep 17 2020 at 12:46):

Dunno, but without a use case the motivation is 0 ;-)

view this post on Zulip Cyril Cohen (Sep 17 2020 at 13:17):

As @Xuanrui Qi said it might be necessary once you get to any category of some class of categories, (and one gets there really fast)

view this post on Zulip Bas Spitters (Sep 17 2020 at 14:50):

I haven't looked at this carefully enough, but is math-comp suitable for this?
E.g. choicetypes seem somewhat unnatural when working with universes.

view this post on Zulip Xuanrui Qi (Sep 17 2020 at 18:02):

I'm not at the stage of working with choiceTypes yet, but since I'm doing everything classically every type is a choiceType. I guess that simplifies part of the problem

view this post on Zulip Karl Palmskog (Sep 17 2020 at 18:09):

hmm, I think one might differentiate between:

  1. category theory using packed classes, in any way possible
  2. category theory integrated with MathComp generally, following the MC encoding style and existing hierarchies

It seems to me 1. is possible/feasible, but like Bas I'm skeptical of 2., i.e., whether it's a good idea to hook into the existing MC hierarchies (after having looked at all the exotic encodings used in other Coq category theory libraries).

view this post on Zulip Enrico Tassi (Sep 18 2020 at 08:14):

If you start from scratch (I mean, not plugging your structure into MC's hierarchy) then it would be really nice to try to use Hierarchy Builder for this, and would motivate me to add full support to universe polymorphism, which is today absent.

view this post on Zulip Xuanrui Qi (Sep 20 2020 at 14:50):

For those who may be interested, I have created a Element/Riot chatroom (https://matrix.to/#/!xRGtNQXoZBhMCllIEL:matrix.org?via=matrix.org) to discuss issues relating to developing category theory/topos theory/algebraic geometry in Coq/MathComp.

view this post on Zulip Bas Spitters (Sep 20 2020 at 14:58):

Interesting, but why yet another communication channel?

view this post on Zulip Cyril Cohen (Sep 21 2020 at 16:55):

Indeed, I suggest we keep discussing it on the math-comp users stream on zulip, and if the conversation happens to span too many topics, we might open up a new dedicated stream. @Xuanrui Qi wdyt?

view this post on Zulip Xuanrui Qi (Sep 21 2020 at 16:56):

We can also keep it here. We (me and Reynald) already use Element for several other projects so it was convenient for us, but if others think otherwise we should keep it here.

view this post on Zulip Xuanrui Qi (Sep 22 2020 at 09:11):

The category theory part at: https://github.com/xuanruiqi/categories


Last updated: Jan 29 2023 at 19:02 UTC