Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: community: general

Topic: Category database


view this post on Zulip John van de Wetering (Aug 12 2020 at 12:50):

Is there some resource online somewhere that lists useful properties of certain often-used categories?
I imagine it would be Wiki-like and have a page for each common category and then a list (possibly with references) of properties that category has.
Like, for Sets it would say it is complete, cocomplete, is a topos, every mono splits, etc.

view this post on Zulip Oscar Cunningham (Aug 12 2020 at 12:52):

I once saw an attempt at making such a Wiki, but it didn't take off. I do keep seeing people ask for such a thing though, so there's clearly demand for it.

view this post on Zulip Oscar Cunningham (Aug 12 2020 at 12:53):

Could the same thing be accomplished by adding more information to the nLab?

view this post on Zulip John van de Wetering (Aug 12 2020 at 12:56):

I think so

view this post on Zulip John van de Wetering (Aug 12 2020 at 12:58):

nlab has a page for the category of Sets for instance https://ncatlab.org/nlab/show/Set

view this post on Zulip John van de Wetering (Aug 12 2020 at 12:58):

But it doesn't mention a lot of properties beyond the topos-theoretic

view this post on Zulip John van de Wetering (Aug 12 2020 at 13:01):

A different resource that might be useful to quickly find counter-examples would be something like https://topology.jdabbs.com/ but for categories.

view this post on Zulip Thibaut Benjamin (Aug 13 2020 at 09:46):

I agree that probably the easiest way to do it is to add information on an existing structure such as the nlab. I actually don't know much of how to edit it, but maybe it is possible to create a page or a category "dictionary of commonly used categories" with references to individual pages for each of the categories. I guess if anyone do this, it would be best to come up with a page which has already substantial content, so that the added value is obvious and there is no risk for the page to get deleted. Maybe here would be a good place to browse some ideas for such a page/write a draft?

view this post on Zulip Jules Hedges (Aug 13 2020 at 09:53):

See also: https://mathoverflow.net/questions/68442/what-could-be-some-potentially-useful-mathematical-databases

view this post on Zulip Jules Hedges (Aug 13 2020 at 09:54):

There are many subjects that would benefit from a database like this, and very few that actually have one

view this post on Zulip Oscar Cunningham (Aug 13 2020 at 09:56):

The nLab has a very confusingly named page Category — category.

view this post on Zulip Oscar Cunningham (Aug 13 2020 at 09:57):

That lists all the categories that nLab has pages about.

view this post on Zulip Thibaut Benjamin (Aug 13 2020 at 10:22):

Oscar Cunningham said:

The nLab has a very confusingly named page Category — category.

That looks a bit like what I had in mind, maybe that could be a good start. I agree that the name of the page is pretty terrible, and I think these should be sorted in different sections instead of being just a big list. Maybe a also a one sentence description following each of the links would make the page a little more friendly

view this post on Zulip Thibaut Benjamin (Aug 13 2020 at 10:30):

Jules Hedges said:

There are many subjects that would benefit from a database like this, and very few that actually have one

Unfortunately, it seems that there is very little we can do about it, I don't believe anyone has enough influence to start a project that would reach to every community. But as a community, we can do our best to maintain such a database, and hope that will inspire other community to create maintain such resources, possibly at the same place - that's why I believe taking advantage of the nlab is also great, the more centralized the information is, the easier it is to find it

view this post on Zulip John Baez (Aug 13 2020 at 14:53):

Oscar Cunningham said:

The nLab has a very confusingly named page Category — category.

Yeah, wikis of this sort have "categories" - you can put any page in some category X just by writing

category: X

at the bottom of the page And if someone sees this at the bottom of the page, and clicks on it, they go to the automatically-created the wiki page listing all pages in that category, which is naturally called

Category - X

This is a bit confusing when your wiki is about category theory, but I'm sure category theorists can handle a category called "category". :upside_down:

So if you go to any nLab page about a category, like my current favorite, SupLat, you'll see

category: category

and if you click on that, you go to the page listing all pages about categories!

Category - category

And there are 84 today.

at the bottom. And if you click on it, you go to the automatically-created the wik page listing all pages in that category, which is naturally called

view this post on Zulip John Baez (Aug 13 2020 at 15:04):

Thibaut Benjamin said:

Oscar Cunningham said:

The nLab has a very confusingly named page Category — category.

That looks a bit like what I had in mind, maybe that could be a good start. I agree that the name of the page is pretty terrible, and I think these should be sorted in different sections instead of being just a big list.

Now I hope you see why the name of the page has to be this, and why it's just a big list - it's automatically generated.

If you want to create another page that's a kind of database of categories, that's easy to do. And the nLab already knows 84 categories that should be in this database. You can format the database in any way you want, and you can easily link to the nLab pages on these 84 categories so that by clicking on them readers can go to those pages. And this important, because while some information is nicely presented on a database, it's also nice to read articles about individual categories, and these have already been written.

view this post on Zulip Joshua Grochow (Aug 15 2020 at 19:38):

I think a really awesome example to try to emulate here is GroupProps https://groupprops.subwiki.org/wiki/Main_Page . It's a community wiki, but being specifically for this purpose (unlike, say, nLab which is much broader in scope) its data is much more structured. It started out small, with essentially one person, but now it's pretty awesome, and the added structure is super useful.

view this post on Zulip Tim Hosgood (Aug 18 2020 at 17:12):

cf https://math.stackexchange.com/q/1639034/71510 :smile:

view this post on Zulip Oscar Cunningham (Aug 18 2020 at 17:13):

Hey look, there I am! I remembered that post but I couldn't find it again when this topic came up.

view this post on Zulip Tim Hosgood (Aug 18 2020 at 17:13):

i always hoped that such a thing would be like some of the currently existing databases of algebraic geometry objects and topological spaces, that let you search by boolean combinations of properties (eg is_cartesian_closed && !is_abelian)

view this post on Zulip Tim Hosgood (Aug 18 2020 at 17:16):

if anybody is interested in starting this then i’d be very keen on helping with some of the behind-the-scenes web dev stuff

view this post on Zulip Tim Hosgood (Aug 18 2020 at 17:16):

i think i came up with some vague ideas back when i asked that SE question

view this post on Zulip John van de Wetering (Aug 20 2020 at 17:23):

All the code for pi-base is on github. So in principle we could take that, rename "space" to "category" and we would be pretty much set on the infrastructure department right?

view this post on Zulip Cole Comfort (Aug 20 2020 at 18:06):

I feel like it might actually be harder to find a relatively modular way to categorise different types of properties than the data entry itself. Like different properties stack up in different ways.

view this post on Zulip Cole Comfort (Aug 20 2020 at 18:08):

Like consider monoidal closedness. Ideally this would be associated both with being monoidal and being closed in the way that the database is constructed.

view this post on Zulip Cole Comfort (Aug 20 2020 at 18:14):

And a categories can have different monoidal structures/closed monoidal structures to make things even more complicated.

view this post on Zulip Dan Doel (Aug 20 2020 at 18:18):

Can a category be monoidal closed in two different ways? At most one of them would correspond to being closed in the sense definable without a choice of monoidal structure, right?

view this post on Zulip Cole Comfort (Aug 20 2020 at 18:20):

Hmmm I am thinking of how a category can be compact closed with different cups/caps, but I suspect that they may always be isomorphic

view this post on Zulip Dan Doel (Aug 20 2020 at 18:21):

Just 'closed' might be more flexible than I thought.

view this post on Zulip Nathanael Arkor (Aug 20 2020 at 18:21):

A category can have multiple nonequivalent closed structures.

view this post on Zulip Dan Doel (Aug 20 2020 at 18:21):

I thought it was somehow reflecting the hom more fully than it actually is.

view this post on Zulip Thibaut Benjamin (Aug 21 2020 at 15:48):

So if we were to take a very systematic approach about this and list categories with respect to their properties, we would have to enumerate all the non-isomorohic closes structures that exist on each of them? That doesn't sound that something very practical either to do, or to search. On the other hand, it seems unsatisfactory to leave out the structure entirely and not mention the possible closed structures (at least the common ones) on various categories.
To be honest, it is not very clear to me how to organize all this data in a manageable way, that allows for easy navigation, and that account for the additional structures one can put on a category

view this post on Zulip Thibaut Benjamin (Aug 21 2020 at 15:52):

Maybe we could have separate databases for each categories equipped with a relevant structure (e.g. a database for monoidal closed categories), with, for each entry an attachment to the underlying category in the database of categories. Then, when consulting an entry in the database of categories, it could run a quick search in the database of monoidal categories to indicate what are the (most popular) monoidal categories with this precise category as its underlying category (I.e. the monoidal structures on this category)

view this post on Zulip Ralph Sarkis (Aug 21 2020 at 18:21):

In that case, it would be worth to also include functors, natural transformations, monad structures over a functor, adjunctions, and so on. I feel like all this data could very intuitively be coded as objects as in object-oriented programming. For example, the "class" Functor has properties like source, target, isFaithfull, etc.. while the class monoidal closed structure has properties like carrierCategory, isSymmetric, isBraided, etc... Then, when you look for a category that is monoidal closed which has some other property P (not relevant to the monoidal closed structure), you first look into all monoidal closed structure and then check if the object carrierCategory has property P. I believe this works for most of the objects I have studied in category, for instance there can be multiple monad structures on a functor, or there can be several categories equivalent to one another. Nevertheless, I am sure people will come up with an easy counterexample I have not considered .

Unfortunately, I don't know anything about databases and I have no idea how feasible or efficient a system like this could be. There are however database systems that seem to be working with this kind of data: https://en.wikipedia.org/wiki/Object_database.

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 18:46):

In this flavour, there's also
https://en.wikipedia.org/wiki/List_of_lists_of_lists

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 18:47):

@Joshua Grochow I thought the groupprops page is just one guy. Is there a way to see who contributed and how much, etc.?

view this post on Zulip Joshua Grochow (Aug 21 2020 at 18:52):

It started as just one, but I believe anyone can sign up to edit the wiki. Why does that matter though? It seems like the setup is a good mix of structure and flexibility that's been talked about in this thread. And just based on this thread it seems like there would be plenty of contributors.

One nice thing about the groupprops wiki: it's very structured, but you don't have to decide on the monolithic structure of a database ahead of time (the some in this thread seem to be trying to do). Rather just some ideas of organization, and the rest emerges organically

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 18:59):

Bildschirmfoto-2020-08-21-um-20.55.01.png

I try to be as dedicates as possible in my own notebook to point out the other already existing notions (other notebook entires) that are used in the definitions. At one point I had it dynamically synched with a graph where I can move around and jump into the wiki entires.

As for categories, there's a lot of ways in which you can write down and how objects can bend their definitions (strict, lax, up to this and up to that), so I found it hard myself to find a balance. Is a limit defined in terms of some cones, what are those cones, or is it some initial/terminal arrow from some functor to/from the diagonal functor, do I have type system underlying. What about the logic, domains of discourse, etc. Scary.

view this post on Zulip Eduardo Ochs (Aug 21 2020 at 19:13):

I think that it would also be great to have a database of categorical _constructions_ and ways to visualize them... there are hundreds of interesting constructions that were published in a very terse way, but since then it became much easier to typeset and share diagrams, and people published in blog posts, notes, slides, and obscure preprints their own ways of understanding these constructions, but this material is hard to find...

view this post on Zulip Eduardo Ochs (Aug 21 2020 at 19:26):

@Nikolaj Kuntner, how do you edit that graph of notions? I just found your wiki and your youtube channel, but they're both huge... is that explained there?
https://axiomsofchoice.org/
https://www.youtube.com/channel/UCcrSMnEYhIPX_p127jI23qw/videos

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:12):

@Eduardo Ochs Bildschirmfoto-2020-08-21-um-22.06.06.png
Nevermind that Wiki, I haven't updated that in many years and it's just there to share my contatcs as I'm not university affiliated anymore.
I still take notes in that style, but I wrote a tiny flask server (python) and use it locally. I think DokuWiki works nicely, although it has too many wizzles for a single user. I've seen physicists use tiddlyWiki, which is more compact, but parsing a text file to html like in the pic is easy enough and features like opening the files in an editor and such can be done in a few thousand lines. But I figure a lot of people know the nLab software already, so why not use that?
In any case, what you describe sounds too much like the nLab already - and the formalized version sounds like it will only look like something in 15 years tbqh.

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:14):

I show how you can drag a textfile into a broswer and have its LaTeX rendered via MathJax here

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:14):

https://youtu.be/bk0J7WGwk90

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:16):

The arrows in the graph are literally just Wikipedia style links [[other_page]] and the software I had used was graphviz.
https://graphviz.org/

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:51):

Also, I just remember I did a paper review on a group in the field of Mathematical Knowledge Management some months ago
https://youtu.be/Pp85jeBCDmc

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:51):

Apart from some stuff you guys brought up (nLab, libraries associated with provers), they survey and keep track of things like

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:51):

https://www.lmfdb.org/

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:52):

(LMFDB - The L-functions and Modular Forms Database)

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:53):

Bildschirmfoto-2020-08-21-um-22.53.10.png here's a screenshot from a page in that paper, maybe you find some inspiration

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:54):

Bildschirmfoto-2020-08-21-um-22.54.04.png I see my notes on the paper end up with the start of a list of things that aren't there (sorry for the screencap dump)

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:55):

http://cantorsattic.info/Cantor%27s_Attic
I know this is (was!) a Wiki on large cardinals, I think it's actually by Hamkins

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:56):

You wouldn't know since the server seems to have an issue for over a year now and the site is broken

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:56):

But from personal anectotal evidence I can promise you he talked about various infinities there

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 20:57):

And I remember Andrej Bauer is another mathematican who has a dozens of different zoology projects

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 21:02):

In another life I also looked into the work of William M. Farmer, who I'd say is/was into lisp and he tried to formalize frameworks for MKM (Mathematical Knowledge Management). That involved type theories with undefind binders (formally related to the Bourbaki-tau or Hilbert epsilon I think) or something something sheafs representing mathematical concepts and organizing them. One can probably go infinitely deep in that "framework direction"
Here's that lisp like type system proposal
https://arxiv.org/pdf/1305.6206.pdf
iirc he says it interprets Gödel-Bernays set theory in some sense

view this post on Zulip Nikolaj Kuntner (Aug 21 2020 at 21:06):

Bildschirmfoto-2020-08-21-um-23.05.26.png If one really wants to go formal, here's a survey paper (prover related) with funky graphs https://arxiv.org/pdf/1912.03028.pdf

view this post on Zulip John van de Wetering (Aug 22 2020 at 23:05):

Cole Comfort said:

I feel like it might actually be harder to find a relatively modular way to categorise different types of properties than the data entry itself. Like different properties stack up in different ways.

If you want a comprehensive list of structures on categories as a reference then this becomes an issue indeed. If you just want to have a database to look up some quick counter-examples, then a more bare bones architecture would do I think. E.g. you can just say that a category is monoidal closed, and then in a note to this property add to which monoidal structure this refers.

view this post on Zulip John van de Wetering (Aug 22 2020 at 23:06):

A potential problem with designing such a database is that since we are all mathematicians, we might over-engineer it :P

view this post on Zulip Cole Comfort (Aug 22 2020 at 23:31):

John van de Wetering said:

Cole Comfort said:

I feel like it might actually be harder to find a relatively modular way to categorise different types of properties than the data entry itself. Like different properties stack up in different ways.

If you want a comprehensive list of structures on categories as a reference then this becomes an issue indeed. If you just want to have a database to look up some quick counter-examples, then a more bare bones architecture would do I think. E.g. you can just say that a category is monoidal closed, and then in a note to this property add to which monoidal structure this refers.

One could just only list off properties and not structure... things could be made a lot easier

view this post on Zulip John Baez (Aug 23 2020 at 05:42):

Nathanael Arkor said:

A category can have multiple nonequivalent closed structures.

Yes. Here's a nice result: there are exactly two symmetric monoidal closed structures on the category Cat, up to equivalence. One is the usual cartesian closed structure; the other comes from the funny tensor product of categories.

view this post on Zulip John Baez (Aug 23 2020 at 05:44):

There are shitloads of symmetric monoidal structures on Set, but I forget how many symmetric monoidal closed structures there are. I'll wildly guess that there's just one, up to equivalence.

view this post on Zulip Nikolaj Kuntner (Aug 23 2020 at 11:40):

So, why not just be more active with examples on the nLab? Contrapoints?

view this post on Zulip Tim Hosgood (Aug 23 2020 at 14:16):

for me, the nLab is just lacking this search functionality: I always imagined something a bit like Counterexamples in Topology

view this post on Zulip Nikolaj Kuntner (Aug 23 2020 at 14:30):

But isn't that just a matter of Example sections? The nLab already has pages named after the concepts for which you'd want examples.

view this post on Zulip Nikolaj Kuntner (Aug 23 2020 at 14:41):

Bildschirmfoto-2020-08-23-um-16.35.31.png
The way I had generated the graph was just from the links in dedicated places, all deriving from the pages files that are apriori independent of it.
My thinking is that if the pages (nodes) are predicates and the arrows (edges) are subset, actually capturing theorems,
{-4,0,4,8,12,...} ==> {-4,-2,0,2,4,6,8,10,12,...}
you actually express a sort of internal language.

view this post on Zulip Nikolaj Kuntner (Aug 23 2020 at 14:47):

"a topos is also, in particlar, a cartesian closed category"
is an arrow instantiated by cleaned up example section you can non-ambiguous parse from.

view this post on Zulip Morgan Rogers (he/him) (Aug 23 2020 at 15:47):

This is the kind of visual structure I've been wanting for a long time, although it always ends up frustratingly crowded in 2D. The best way to make it effective, imo, is to not try to cram everything into a single diagram. Or try to cram all of these suggestions into an all-encompassing database, for that matter. If any of these database ideas take on an existence, whether within or independent of the nLab, it would be straightforward to interlink them at that point.

view this post on Zulip Nikolaj Kuntner (Aug 23 2020 at 16:06):

Bildschirmfoto-2020-08-23-um-18.01.57.png
Very true! The graphviz library does feature a few regroupings (spring, top-bottom, left-right, etc. shown in this pic, which is the same data of the entries around "Functor"), but when you plot hundreds of pages, it takes forever to move around at any workable resolution.
My idea (never coded up) was to compute the Upper set and Down set (in the sense of filters on a poset) for the subset graphs, to any depth you're interested in.
That would help, but to dynamically recompute the info while aping around between the branches, it would require some serious user interface design effort.

view this post on Zulip Antonin Delpeuch (Aug 28 2020 at 12:48):

It could be interesting to use Wikibase for this. It is a form of wiki where data is input in structured form, like this: https://www.wikidata.org/wiki/Q168620. Wikidata is a general-purpose instance of Wikibase, but we could have one specifically for category theory, with our own concepts. The ontology (properties used to describe objects) are user-defined, so there is a lot of flexibility built-in. It also comes with a powerful query language (SPARQL), which can be used to generate all sorts of visualizations from the data: https://w.wiki/QEW.

view this post on Zulip Antonin Delpeuch (Sep 06 2020 at 16:05):

I had a go at linking Wikidata and nLab better, and that lets you visualize the graph of subclasses between the concepts represented in the nLab. Result (heavy webpage!): https://w.wiki/bRw

view this post on Zulip Antonin Delpeuch (Sep 06 2020 at 16:26):

This graph can be edited: if you see missing relations, you can just add a "subclass of" property on the corresponding item, like this: https://www.wikidata.org/wiki/Q2943034

view this post on Zulip Morgan Rogers (he/him) (Sep 06 2020 at 16:53):

That's a very pleasing mess! Nice one!

view this post on Zulip John van de Wetering (Sep 06 2020 at 17:00):

That's really cool! Can you explain a bit more how this works under the hood?

view this post on Zulip John van de Wetering (Sep 06 2020 at 17:02):

I like how after the graph settles itself you can zoom out and really easily see what the fundamental concepts are: they are sort of isolated looking nodes with a lot of arrows pointing towards it.

view this post on Zulip Antonin Delpeuch (Sep 06 2020 at 21:16):

The visualization is generated by a SPARQL query that you can see by clicking the "Edit SPARQL" link on the right-hand menu of the visualization. The query generates the graph edges by requesting all pairs of Wikidata items which are both linked to the nLab, and one is marked as a subclass of the other. All the underlying data is editable (even without creating an account) - for instance Wikidata did not know about bimonoidal categories so I have created https://www.wikidata.org/wiki/Q98931512, linking it to the nLab and relating it to other items.

view this post on Zulip Nikolaj Kuntner (Sep 07 2020 at 17:50):

Pretty cool. How tightly is this dependent on the Wiki data, can it be more or less easily be used as standalone for just nLab?

view this post on Zulip Antonin Delpeuch (Sep 08 2020 at 09:25):

Yes it is possible to run independent instances of that software (Wikibase). Either manually (for example with https://github.com/wmde/wikibase-docker) or from hosting providers (https://www.wbstack.com/, https://professional.wiki/en/hosting/wikibase). I could help set one up if people are interested :)

view this post on Zulip Nikolaj Kuntner (Sep 08 2020 at 18:53):

I'm interested in trying to find out how it works, e.g. running it locally on a small set of data

view this post on Zulip Valeria de Paiva (Sep 08 2020 at 21:44):

Antonin Delpeuch said:

I had a go at linking Wikidata and nLab better, and that lets you visualize the graph of subclasses between the concepts represented in the nLab. Result (heavy webpage!): https://w.wiki/bRw

hi @Antonin Delpeuch , this is really great!
I also wanted a better mapping between the nLab and WikiData, so I'm really pleased, thanks!!!
But I am also a bit surprised: when I look your graph and query, it seems to say that there are

Showing 1 to 200 of 623 rows rows per page

only 623 rows and I know we have some 10.5 K pages of non-humans in the nLab. so, it seems that 623 is too low a number.
(I am only looking at the stuff produced by your query).
is this reasonable do you think? how many mathematical concepts do you think WikiData has? do you know the number for Wikipedia? Do you have other stats that you're willing to share? Many thanks!

view this post on Zulip Antonin Delpeuch (Sep 10 2020 at 09:49):

@Valeria de Paiva absolutely! At the moment there are 15k pages on nLab, and 3.4k of them are linked to Wikidata via the dedicated property (https://www.wikidata.org/wiki/Property:P4215). So there is a lot of room for improving this linkage :) The reason why the query returns 623 results is that each result corresponds to an edge in the graph, so you only get one per pair of nLab concepts for which we have a known "subclass of" relation. For instance, nLab has pages about people, and on Wikidata those do not have such relations, so they are excluded from the results. There are also concrete instances of these concepts (such as the category of sets https://www.wikidata.org/wiki/Q2518298) which are just "instances of", not "subclasses of" other notions, and therefore do not appear in my query (but it could probably be tweaked to show them too).

To improve this, we can:

view this post on Zulip Antonin Delpeuch (Sep 10 2020 at 12:47):

@Nikolaj Kuntner then I recommend the Wikibase-Docker setup, if you have docker install you can spin up a local instance in minutes, with all the bells and whistles :)

view this post on Zulip Valeria de Paiva (Sep 10 2020 at 14:20):

@Antonin Delpeuch many thanks!!! after writing I had found the info about the 3.4K nLab pages connected in the documentation page https://www.wikidata.org/wiki/Property_talk:P4215.