While a colimit is of a typical object in category theory hence so much in the closely related areas such as categorical logic and type theory, its construction can be a nuisance especially within a strict category setting where elementhood matters in the objects.
We describe a concrete method of “generating an element of colimit” in terms of so called solution set as a part of necessary and sufficient conditions of adjoint functor theorem.
While the idea is not original and the contents are parallel to the CWMMacLane, S. (1971). Categories for the Working Mathematician. New York: Springer-Verlag., we believe that the exposition is helpful and unique in the applicable interpretation.
1. The solution set condition and its interpretations
The solution set condition, originally formalized as a necessary condition that a functor (under some condition) becomes right adjoint, is an interesting assertion by itself simply because it gives an explicit construction of a colimit.
More precisely, solution set condition denotes the existence of “weakly universal objects” in some sense that can be expressed (or unified) in terms of functor involved with the following (general) adjoint functor theorem and its corollaries:
- Adjoint functor theorem;
- Condition for the existence of initial object;
- Representable functor theorem.
Although we are not giving any proofs and unnecessary only for the exposition, we denote by a locally small, complete small category. We also fix a functor where the selection of a category is the key to characterize what the solution set is for. We persist in these notations throughout the part 1.
With these in mind, the (unified) solution set condition is concisely stated as:
Here wInit denotes a (small) set of weakly initial objects, whose element suffices the condition of initial object except the uniqueness condition.
(*S) can be stated explicitly as:
(*S) is exactly the solution set condition for adjoint functor theorem, the condition will be interpreted accordingly in a context.
1.1. Condition for the existence of initial object
By setting , dropping and letting the constant functor, we obtain a necessary condition for the existence of initial object, namely:
Notice that canonically preserves every (small) limits because any universal cone collapses to the zero object in .
1.2. Representable functor theorem
This is analogous to the condition for the existence of initial object.
For , a representation of is identified with the universal arrow , or equivalently the unit of adjoint , where is identified with the faithful subcategory and the composition of followed by , furthermore a choice functor.
Therefore is representable if and only if and preserves small limit.
2. Subobjects and spanning maps
For an arbitrary category , we can consider “subobjects” of an object , whose elements are monos together with the order relation defined by if and only if there exists some and a mono such that , or to say concisely factors through . By defining , we call the set of equivalence classes subobjects of a. We denote subobjects of a by .
Definition 2.1. For a given functor , a map is said to span a when there is no (non-isomorphic) mono such that factors through .
Lemma 2.2. Fix a category and its object .
Suppose the pullbacks for any set of subobjects exists, namely . If a functor preserves any of such pullbacks, then every map factors through a map that spans .
Proof of lemma 2.2. For , let be a set of subobjects such that with for each i. Since by assumption there exist the pullback which we denote as , we see it suffices , where is the induced map on pullback diagrams of .
apparently spans by the construction of ; precisely, if there is a mono such that factors through for some (i.e. ), then must be in and since is the pullback, must coincide with , analogously with and with .
3. A general method of constructing a colimit as the result of a left adjoint functor from Set
It is an immediate consequence of adjoint functor theorem that we have a general method to construct a colimit of certain type in a particular class of categories.
The applicable class of categories represented by should suffice the following properties
- is locally small and complete small;
- It is given a continuous functor to ;
- suffices solution set condition
Not exclusive yet particularly important instance of such classes is the algebraic system of fixed type, which forms a category of algebra of given type . suffices
(*AFT) along with the functor known as forgetful functor .
If we are given such functor with these properties, adjoint functor theorem states that the continuous functor admits a left adjoint, which preserves a colimit of , hence the image of the left adjoint is the constructed colimit in .
Moreover, this construction procedure can be done in an algorithmic manner. Above lemma shows that, the solution set of can be identified with the union set of maps that span from . This can be seen as follows:
To a given map , choosing a map through which factors is equivalent to inducing a (part of) pullback map in the diagrams of the form .
This last description roughly speaks of algorithmic nature of a (co)limit preserving condition of procedure (i.e. functor), namely providing with a “basis” in the target category against an arbitrary object of source category.
Here we mean by “basis” is a set of objects that admit irreducibleness of some sort (c.f. might be preferable to express as “atomicity” in a context).
Here is an example.
3.1. Coproduct in Grp
In , the forgetful functor admits the free group construction as the left adjoint, where a solution set of is composed of every monomorphisms of the form that has no factoring monos through a subgroup . Hence plays a part of freely generating (as a group) set for .
The free construction preserves colimit (direct sum) of , hence the coproduct is justified to have the form in , meaning that an element of is obtained by (finite applications of) group operations and identities on the base set in terms of universal algebra.
|↑1||MacLane, S. (1971). Categories for the Working Mathematician. New York: Springer-Verlag.|