Add support for other categorical structures

[varkor]

In addition to categories, it would be useful to be able to add entries and properties for structures such as functors, natural transformations, 2-categories, double categories, (infinity, 1)-categories, and so on. While it would presumably require a few changes to the structure of the current data format, the system seems flexible enough to support this without too much additional effort.

[ScriptRaccoon]

Thank you for the suggestion.

Long ago I already tried to incorporate information about special types of morphisms: regular monomorphisms, split monomorphisms, effective monomorphisms, etc. There are also implications between these properties of morphisms, and counterexamples. This should still be findable in the commit history. However, I removed it again because it didn't really fit with the rest of the application. In the end, this would just become a collection of examples and counterexamples for properties of monomorphisms (and epimorphisms), the database probably would not save any specific morphisms, which is a huge difference to what CatDat currently is.

Following your suggestion, I would start with the simplest case: functors. But I am afraid it would turn into the same situation. I don't think it makes much sense to store specific functors in a database. Again, it would amount to a collection of examples and counterexamples, e.g. a fully faithful functor that is not essentially surjective, or a functor that preserves finite limits but not all limits. Somehow, it doesn't feel right to include this in CatDat.

You suggested higher categories, and my objections do not apply to them. However, I am concerned that it would be quite difficult to add, say, 2-categories to the application and (a) include a sufficiently large number of examples of 2-categories (so that it is worthwhile), (b) include a sufficiently large number of properties of 2-categories, and (c) keep the UI clear and easy to use.

[varkor]

Again, it would amount to a collection of examples and counterexamples

I don't think I quite follow. Isn't this precisely the focus of CatDat at the moment? E.g. the search feature specifically allows you to search for categories satisfying property X but not property Y. I suppose it's not clear to me what argument applies to functors that does not apply to categories.

However, I am concerned that it would be quite difficult to add, say, 2-categories to the application and (a) include a sufficiently large number of examples of 2-categories (so that it is worthwhile), (b) include a sufficiently large number of properties of 2-categories, and (c) keep the UI clear and easy to use.

Regarding (a), there are "more" examples of 2-categories than of 1-categories (trivially, since every 1-category is a 2-category, and also because essentially every concept in 1-category theory can be extended, typically in several ways, to 2-category theory). So certainly a sufficient number of examples exist. There is a question of whether people will be motivated to contribute enough of them, but this applies in general to CatDat. I would be keen at least to add plenty of examples of double categories.

Regarding (b), I think the same comment applies. Pretty much every property of 1-categories has several analogues for 2-categories.

I understand the concern in (c), but I think it should not add much overhead. For instance, the "Categories" tab could become a "structures" tab, with an input field at the top to filter by kind of structure (and similarly for properties, which would be relative to the kind of structure). Then each individual page would be no more complicated (apart from some annotation somewhere saying what kind of structure it is).

[ScriptRaccoon]

I see. Maybe I can give it a try.

I still think there is a crucial difference between categories and, say, functors as for the database. A functor usually only acts as a device to "communicate" between categories, they are usually not interesting in their own right. (From a practical standpoint, of course every category $\mathcal{C}$ can also be seen as a functor $1 \to \mathcal{C}$.) Because of this, I think that the community does not need a "list of functors" in the same way as a "list of categories".

But indeed: it would be nice to have a functor property combo search.

So here is a suggestion what to do next:

• Rename existing table properties to properties-for-categories. Rename table category-properties to category-property-pairs. Same for non-properties. Rename table implications to category-implications. This is to avoid confusion with what comes next and to make it scalable.
• Add new tables: functors, properties-for-functors, functor-property-pairs, functor-non-property-pairs, functor-implications.
• Fill the tables properties-for-functors (see below) and functor-implications.
• Fill the table functors: not as an attempt to list all interesting functors, but to provide witnesses for functors which have property P but not property Q (if that is consistent).

Some ideas for properties-for-functors:

• preserves limits
• preserves products
• ... same with all other types of limits and colimits
• is a right adjoint
• is an isomorphism (evil!)
• is an equivalence
• is fully faithful
• is faithful
• is full
• is essentially surjective
• is conservative
• creates limits
• reflects limits
• is monadic
• is comonadic
• is accessible
• is dense

Some implications:

• isomorphism => equivalence <=> fully faithful + essentially surjective
• is a right adjoint => preserves limits => preserves products + preserves terminal object + ...
• monadic => is a right adjoint

Let me know what you think.

[ScriptRaccoon]

I have created this PR to add functors.

#12

[varkor]

First, I think that a "functor property combo search" would be very useful, and the examples you give are definitely a good starting point!

I think there's one aspect I still don't follow.

In the contribution guidelines, one of the criteria for adding new categories is "New Combinations". This suggests that the motivation for adding new categories to the database is to provide examples/counterexamples of property combinations, rather than to serve as a reference for the properties that a specific category has.

From this perspective, I would have expected categories and functors to behave the same way in the interface: that is, it is not clear to me why individual categories should have their own page, if their purpose is to exhibit unique combinations of properties.

I think it is true that people will more often want to look at the properties a specific category has than properties a specific functor has, but I do think it is useful to look for the properties a specific functor has. For instance, some functors have surprising properties (e.g. the fact that Abelianisation preserves finite products).

Furthermore, the ability to have multiple witnesses of a combination of properties for functors may suggest patterns that lead to useful abstraction and conceptual understanding, that would not be aided by simple having a binary indicator for "consistent"/"inconsistent".

[rschwiebert]

In DaRT, we use "related" rings to drive some of the logic. Say if, R is-subring S, then all the properties that pass to subrings are passed positively down to R if present in S, and negatively up to S if R lacks them. Whenever you encounter a subring that has P but its superring does not have P, it can be listed as a counterexample for that metaproperty's inheritance.

Having pairs of categories related by various flavors of functors and spreading the inheritance this way (if you're not already doing it) would probably result in many more deductions.

[varkor]

What are some examples of properties of categories are inherited/bestowed by those of subcategories?

[rschwiebert]

What are some examples of properties of categories are inherited/bestowed by those of subcategories?

I'm not the best person to ask, but to give a trivial example of what I was expressing, a subcategory of a thin category would be thin. There are probably examples where subcategories bestow something on a supercategory (which I think is what you were asking specifically.). Of course, it can be phrased using an inclusion functor. The whole theme is "ascent/descent" of properties through functors.

And, I imagine, but lack the familiarity with, there are certain properties preserved through full functors, essentially surjective functors, faithful functors, etc, which would contribute their own unique logic based on their character.

There are probably even things you can do along the lines of "is a slice category of" (perhaps that's even expressible as a functor...)

[ScriptRaccoon]

In DaRT, we use "related" rings to drive some of the logic. Say if, R is-subring S, then all the properties that pass to subrings are passed positively down to R if present in S, and negatively up to S if R lacks them. Whenever you encounter a subring that has P but its superring does not have P, it can be listed as a counterexample for that metaproperty's inheritance.

Having pairs of categories related by various flavors of functors and spreading the inheritance this way (if you're not already doing it) would probably result in many more deductions.

While subcategories are probably not the best example in this setting, this is a valid point. I have created a separate issue #22 - let us continue the topic there, not here.

[ScriptRaccoon]

Let me clarify that varkor has convinved me and that you can safely ignore my first comments here!

When the functors PR is done (will still take a while) and the two structures (categories / functors) are refactored and unified to some degree (will take some time as well), the next step would be to add monoidal categories. These were also suggested on zulip, and I would also feel comfortable adding data for these since my past research touched them a lot.

such as functors, natural transformations, 2-categories, double categories, (infinity, 1)-categories, and so on.

I do not yet see much merit in adding natural transformations. Could you elaborate?

But 2-categories could be done after monoidal categories, I agree.

Personally, I don't have enough background in double categories and (infinity, 1)-categories, so for these I could probably only provide the skeleton, not any data.

All these are very long term ideas. CatDat still has unsettled properties for basic examples like the category of rings. I think this has top priority.

It is also important to keep some focus. I assume nothing speaks against multicategories? Oh wait, this also includes operads. Oups, we are making a topology database!

[varkor]

I do not yet see much merit in adding natural transformations. Could you elaborate?

I only mentioned these for consistency. I didn't have particular natural transformations in mind.

Personally, I don't have enough background in double categories and (infinity, 1)-categories, so for these I could probably only provide the skeleton, not any data.

That's fine – the hope is that the community will contribute to CatDat, in any case.

Oh wait, this also includes operads. Oups, we are making a topology database!

I don't think I follow the point you are making here. I agree that multicategories would be natural to include if you are including monoidal categories, but I don't see why this should be avoided simply because topologists also care about such structures.

[ScriptRaccoon]

@varkor The functor PR is ready now: #12

Maybe you want to have a look?