Repository navigation
Add more well-known categories #14
Description
Activity
I assume by hTop you mean the "StrØm homotopy category", i.e. take the category of (all, or maybe just CGWH) topological spaces and identify any two parallel morphisms which happen to be homotopic (this is also the homotopy category of the StrØm model structure).
There is also Ho(Top), the homotopy category of spaces with respect to the "Quillen" model structure (weak equivalences = weak homotopy equivalences). Would be nice to see both in CatDat!
More suggestions:
If I find some time I'll try to learn how the database looks and add these myself.
Reacted by Script Raccoon- added a sub-issue
on May 4, 2026 I have closed #95 because of inactivity and it was targeting a meanwhile old version of CatDat. Here are some facts from that PR that we can reuse when we start this again.
BanAlgu (Banach algebras with unit)
- is complete and cocomplete, this is because of general facts about monoid objects in (co)complete monoidal categories, applied to Ban.
- is not semi-strongly connected because there is no homomorphism between M2 and M3
- is not balanced: The inclusion
$\alpha : C^1([0,1]) \hookrightarrow C([0,1])$ provides a counterexample, where$C^1([0,1])$ is equipped with the norm$||f||_1 := ||f|| + ||f''||$ . Since$\alpha$ is injective, it is a monomorphism. It is also an epimorphism since it has dense image by the Weierstrass approximation theorem. But of course$\alpha$ is no isomorphism.
BanAlgnu (Banach algebras without a required unit)
- is complete and cocomplete, this is because of general facts about semigroup objects in (co)complete monoidal categories, applied to Ban.
For stuff on von Neumann algebras, I have copied this to #71.
I have closed #127 for similar reasons. Here are some facts that we may reuse in a later PR.
SemiNormVect
- has equalizers (like for vector spaces)
- has products (bounded families with sup-norm)
- has coproducts (direct sum with 1-norm)
- has coequalizers (quotient vector space with quotient norm)
- satisfies CIP
- has generator C with usual norm
- has cogenerator C with zero norm
- does not satisfy CSP
- is not balanced (proof is just as for Ban)
- is not unital (proof is just as for Ban)
- monomorphisms are injective
- epimorphisms are surjective
- the forgetful functor SemiNormVect → Vect has a right adjoint: equip a vector space with the zero norm
Also, this category is locally
$\aleph_1$ -presentable by https://mathoverflow.net/questions/511025, but I do not completely understand the proof.NormVect
This has similar properties to SemiNormVect, but of course, epimorphisms are not necessarily surjective, and hence the forgetful functor to Vect has no right adjoint.
Given the CONTRIBUTORS.md guideline adding some categories seems not just a big task but basically impossible. To add hTop for example, I would need to determine whether hTop is mono-regular?
11. Given the CONTRIBUTORS.md guideline adding some categories seems not just a big task but basically impossible. To add hTop for example, I would need to determine whether hTop is mono-regular?
You don't need to.
I agree that adding a category is a bit daunting given all these requirements. I should probably relax these. For me, these days, I only merge a PR for a new category when I have decided almost all properties (Example: #372 + #387). But in principle this can always be done in follow-up PRs. When something is very hard and even AI tools have no idea how to approach it, omit it.
In any case, I don't want anyone to be discouraged of submitting a new category because of the many rules that I have came up with. I would say, though, that at least 50% of the properties should be decided. Is that a good compromise?
One can also always start a PR and then try to collaborate.
While CatDat already has a couple of well-known categories, some are currently missing. Here are some suggestions. Done categories are moved to the bottom.
*either with continuous or uniform maps, not sure yet
Also:
IMPORTANT. Adding these categories to the categories table is easy, but not sufficient, since (see
CONTRIBUTING.md) one should also try to fill in the properties and non-properties (in case they are not deduced already). So this is actually a quite big task. Maybe one can make one commit (or PR) per category.