A protocategory is a way to present a category that makes formal the idea that a single datum (a “protomorphism”) can represent many different morphisms with different sources and targets. For instance, in material set theory, a given set of ordered pairs can represent functions with many different codomains.
As compared to the definition of category with one set of objects and one set of morphisms, a protocategory removes the requirement that each morphism have a unique source and target. As compared to the definition of category with separate hom-sets for each pair of objects, a protocategory requires all these homsets to be (not necessarily disjoint) subsets of one set of all “protomorphisms”.
It is important to recognize, however, that unlike those two definitions of category, a protocategory is not a definition of a category. It retains information about “which morphisms in distinct hom-sets are ‘equal’”, which is not relevant category-theoretic information: in a true category it is never ‘meaningful’ to compare two morphisms for equality unless one already knows for other reasons that their domains and codomains coincide. A protocategory is rather a way of presenting a category, analogous to a group presentation, formalizing the fact that in some cases morphisms in different hom-sets can be “equal” until we “forget about that fact” in a structured way.
A protocategory consists of:
satisfying the axioms
Let the objects be the sets in material set theory (such as ZFC), and let the protomorphisms be sets of ordered pairs such that for any there is at most one such that . The domain of such an is the set of all such that there is such a , and its range is the set of all such that there exists an with . We say if is the domain of and is a superset of the range of . With a suitable definition of composition, this yields a protocategory that generates the category Set.
More generally, if we take the protomorphisms to be all sets of ordered pairs, and to mean that is a superset of the domain of in addition to being a superset of the codomain of , then we get a protocategory that generates the category Rel.
Let the objects be groups, let the protomorphisms be functions, and say that when is a function between the underlying sets of and that is a group homomorphism. This protocategory generates the category Grp.
Any category can be presented by a protocategory in a trivial way, by taking the protomorphisms to be the disjoint union of all the sets of morphisms (i.e. the set in the one-set-of-morphisms definition of category), with the source-target relation being simply a function from protomorphisms to pairs of objects.
It may seem that, at least in a material set theory, we should be able to modify the previous example by taking a non-disjoint union of the sets of morphisms (assuming given a category in the many-sets-of-morphisms definition). However, this is not true, because the composition predicate in a protocategory makes no reference to objects. For example, consider the following category:
Then if we take unions of homsets we have and also , but then the protocategory composition axiom fails: we have and , but there does not exist a unique such that and .
The notion is due to Freyd and Scedrov, Categories, Allegories.
It is recalled in A1.1 of Sketches of an Elephant.
Last revised on April 16, 2018 at 09:34:17. See the history of this page for a list of all contributions to it.