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 CWM[1]MacLane, 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:
While (*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
(*AFT)
:
is locally small and complete small;
- It is given a continuous functor
to
;
suffices solution set condition
(*S)
.
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.
Footnotes
↑1 | MacLane, S. (1971). Categories for the Working Mathematician. New York: Springer-Verlag. |
---|