A comprehensive and searchable database of categorical structures and their properties

Recently added structures

• category of countable-dimensional vector spaces
• category of large vector spaces over a large field with a small basis
• category of long transfinite sequences of abelian groups
• discrete category of sets
• category of set-indexed families of abelian groups

Show more

Structures, Properties, Implications

CatDat currently supports four types of categorical structures: categories, functors, morphisms, and symmetric monoidal categories. Each structure has a detailed description, proofs of its properties (satisfied or unsatisfied), and related structures.

For each type, there is a collection of properties, such as category properties and functor properties. Each property has a detailed description, relevant results, structures satisfying or not satisfying the property, and related properties.

For each type, there is a collection of implications, such as category implications and functor implications, each with a detailed proof. They form the basis of a powerful deduction system that deduces, for every structure, new properties from given ones. Of the 23996 proofs of properties in the database, 22141 have been automated (92%).

Search

CatDat's search feature makes it easy to find structures that satisfy specific properties while not satisfying others. For example, you can find ...

• abelian categories that are not well-powered
• finitely cocomplete categories that have neither a terminal object nor are cocomplete
• cocontinuous functors that do not preserve monomorphisms
• regular monomorphisms that do not split

Any combination of properties is possible. Inconsistent combinations are detected as well (example).

Compare structures

CatDat's comparison feature allows you to compare multiple categories, functors, etc. to identify similarities and differences in their properties. For example, you can compare ...

• rings with commutative rings
• finite sets and countable sets with all sets
• graded modules with cochain complexes
• the contravariant power set functor with the covariant power set functor

Contribute to CatDat

CatDat is a community effort, developed in an open-source GitHub repository.

Whether you're a mathematician spotting missing data or a developer improving the interface, your contributions are welcome. A particularly useful way to help is to fill in missing information in the database.

See how to contribute for more information.