What is a universal property, really?
Universal properties are a convenient method for defining an object in a category up to isomorphism. Rather than giving a concrete, bottom-up construction of an object, we can instead uniquely specify its behavior.
Consider the example of products in a category . We say that the product of and is any object of such that the following diagram commutes.
We say that satisfies the universal property of the product of and .
Surely this matches our set-based intuition of what a product should behave like. Similarly, we can sketch out constructions of other universal properties like initial objects, terminal objects, exponentials, etc. However, what is precisely meant by the term universal property?
The notion of a universal property is made precise by the notion of a universal element of a presheaf. That is, an object satisfies a universal property if we can build a universal element of the appropriate presheaf at that object.
Letβs look at the universal element characterization of the products example. Note that a map into a product is determined by a map into each component. To map into , we need both a map into and a map into , as in the above diagram. That is, to build a map , we must simultaneously provide elements of and at .
Using the product of presheaves, this means we are providing a single element of the presheaf . Quite nicely, the universal element of this presheaf provides the object of that is the product of and . The universal element, provided that it exists, contains the following data:
- An object
- An element
- A proof that the map sending to a pair of maps , is an equivalence. Therefore, any element of factors through
Recall that the product of presheaves is computed pointwise in the category of sets, so if we expand the type of the element above we find that is a pair of maps and .
The first part of this pair is precisely . Correspondingly, the second part of this pair is . Finally, the universality of the element (i.e. the proof that any other element factors through ) captures our commutative diagram from above.
This is a very rough sketch of what a universal property is, and has elided for now an important application of the Yoneda lemma. In any case, all a universal property is really saying is that a particular presheaf is representable; and, rather elegantly, a universal element of a presheaf is convenient packaging of that representability proof.
In summary, universal properties are not as ad-hoc as they may initially seem, and the language of presheaves provides a reusable and precise definition that can be instantiated to describe a very large class of properties.