Property: concrete category?

[catdat-issue-creation]

I don't know if this runs into foundational issues, since it talks about sets. But the definition in terms of a faithful functor into Set seems fairly safe.

I ended up here in the process of trying to understand the correct notion of morphisms for structured sets (a concrete category ought to codify that, right?). I wanted to check, as an illuminating test case, if the category of pointed sets is concrete. It probably is, and I should probably work it out on paper, but it might be nice to have such info in CatDat.

I don't know easy it would be to determine membership for, but it seems like a lot of common categories should be concrete, so maybe there's a useful rule for it. nLab says it's analogous to well-pointedness, but for elements instead of generalized elements?

---

This issue has been created via the submission form on https://catdat.app/category-properties

[ScriptRaccoon]

Yes, concrete (or rather: concretizable, since you are interested in the property) will be added at some point (cf. #18). As a rule of thumb, 99% of categories encountered in practice are concretizable, which is why this property is (a) not so interesting, (b) not very useful, (c) not in the database yet. There are a few exceptions like homotopy categories.

The category of pointed set is concretizable via the obvious forgetful functor to the category of sets.

Regarding the useful rule you mention: every locally essentially small category with a generating set is concretizable. This rule alone covers 93 of the 97 categories recorded in CatDat so far. The only exceptions are LRS, Sch, Z (the category of Z-functors), and BOn (delooping of the ordinals). From these, the first two are also concretizable. But Z and BOn are not concretizable. This is because every concretizable category is locally essentially small.

[ScriptRaccoon]

A more interesting notion is a concrete category as defined as a pair (C,U) consisting of a category C and a faithful functor U from C to the category of sets. This is extra structure, not merely a property. Their theory can be found in the book Joy of Cats. In CatDat this would amount to adding a new structure type, but I don't plan to add this soon.

[ScriptRaccoon]

Meanwhile, the property has been added in #346. I was wrong in claiming that the property of being concretizable is not very interesting. The papers by Isbell and Freyd demonstrate this quite well. Moreover, in #340, Isbell's condition for concretizability was used to show that the new category is not concretizable, rendering the proofs that generating and cogenerating sets do not exist obsolete. When assigning a single property automatically establishes two other properties, it is certainly worth studying.