Colimit

definition example theorem

The colimit of a Diagram $D:\mathcal{J}\to \mathcal{C}$, written $\mathrm{colim}D$, is the universal Cocone: the Initial Object in the category of cocones under $D$. Equivalently it is a representing object for ${\mathrm{Hom}}_{{\mathcal{C}}^{\mathcal{J}}}(D,\Delta (-))$: $[\mathcal{J},\mathcal{C}](D,{\Delta }_x)\cong \mathcal{C}(\mathrm{Colim}D,x)$ (Kittenlab Lecture 9, DaoFP §9.5). 7 Sketches’ “compressed” definition: a cocone in $\mathcal{C}$ is a cone in ${\mathcal{C}}^{\mathrm{op}}$, and the colimit of $D$ is the limit of $D^{\mathrm{op}}$ (Definition 3.102). Kittenlab’s slogan: “colimits are gluing” — take the disjoint union ($n$-ary Coproduct) of the objects, then glue parts together (by equivalence relations, computed with union-find).

Sources: Kittenlab Lecture 9 (“Colimits”), 11, 15; DaoFP §9.5, §10.4, §10.7, §12.6 (“Initial Algebra as a Colimit”), §17.2 (“Colimits as coends”), §19.4; 7 Sketches §3.5.4, §6.2 (Chapter 6 unpacks colimits: initial objects, coproducts, pushouts, finite colimits, cospans), §3.4.4 ($\Sigma$-operations are built from colimits); CTfS §2.6, Definition 4.5.3.25, Examples 4.5.3.28–4.5.3.29, Application 4.5.3.30

Special cases

shape	colimit
empty	Initial Object (in $\mathbf{Set}$, $\varnothing$)
$n$ objects, no arrows	$n$-ary Coproduct
Span $\bullet \leftarrow \bullet \to \bullet$	Pushout
parallel pair $\bullet \rightrightarrows \bullet$	Coequalizer (e.g. $G/H$ for a subgroup $H\le G$ in $\mathbf{Ab}$, coequalizing the inclusion and $0$; angles $\mathbb{R}/2\pi \mathbb{Z}$)
a Preorder as $\mathcal{C}$	Join $\bigvee$; joining systems (Generative Effect)
$\mathbf{Set}$, any finite diagram	disjoint union of the $D(v)$ modulo the equivalence relation generated by $d\sim D(a)(d)$ (7 Sketches Theorem 6.37, Kittenlab)
$!:\mathcal{C}\to \underline{1}$	${\Sigma }_{!}(I)=\mathrm{colim}I$: connected components / quotients (Data Migration Functor)
$\omega$-chain $0\to F0\to F^{2}0\to \cdots$	the Initial Algebra of $F$ (DaoFP §12.6)

Examples from Category Theory for Scientists

• Gluing intervals and spaces (CTfS Examples 2.6.2.2, 4.5.3.29). $[0,1]{\bigsqcup }_{\{1\}}[1,2]\cong [0,2]$; in $\mathbf{Top}$ the pushout of $D^2\hookleftarrow S^1\to \{\ast \}$ collapses the boundary circle of a disk to a point and yields the sphere $S^2$ — “the category of topological spaces has the right morphisms to ensure the result really is a sphere”.
• Transit maps (CTfS Application 4.5.3.30). Model a subway line with $n$ stops as the symmetric line graph $G_n$; a transfer station is a map $G_1\to G_n$ picking a stop. The colimit of a diagram of lines and shared stations, e.g. $G_4\stackrel{4}{\to }{G}_7\stackrel{6}{\leftarrow }{G}_1\cdots$, is the transit map: lines glued at their transfer stations.
• Ologs (CTfS Example 2.6.2.3). “A cell in the torso or arm” is the pushout of “a cell in the torso” and “a cell in the arm” over “a cell in the shoulder”: shoulder cells are counted once. Pushouts can also equate: pushing out “a college course” along “a math course ↦ an utterance of too hard” replaces every math course by that phrase.
• Connected components (CTfS Exercise 4.5.3.26): the colimit of a graph viewed as a functor $(A\rightrightarrows V)\to \mathbf{Set}$ is the Coequalizer of source and target, i.e. its set of connected components; the colimit of the empty diagram is the Initial Object (CTfS Exercise 4.5.3.27).
• Cones as colimits (CTfS Example 4.5.3.28): collapsing the front face $\mathcal{C}\times \{0\}$ of the prism $\mathcal{C}\times [1]$ to a point, i.e. the pushout of $1\leftarrow \mathcal{C}\to \mathcal{C}\times [1]$ in $\mathbf{Cat}$, is the left cone ${\mathcal{C}}^{◃}$ — the shape of all cones.

Properties

• Unique up to unique isomorphism. $\mathbf{Set}$ is cocomplete; C-set categories and graphs have all colimits, pointwise (glue vertices and edges separately).
• $\mathrm{Colim}⊣\Delta$ (DaoFP §10.4); left adjoints preserve colimits (dual); the contravariant Hom Functor turns colimits into limits: $\mathcal{C}(\mathrm{Colim}D,x)\cong \mathrm{Lim}\mathcal{C}(D-,x)$. Colimits are coends and left Kan extensions. Every presheaf is a colimit of representables.
• Isomorphic diagrams have isomorphic colimits (Kittenlab Lecture 15): $F\cong F^{\prime }$ gives $\mathrm{Hom}(F,\Delta -)\cong \mathrm{Hom}(F^{\prime },\Delta -)$, so the representing objects agree — “that’s Yoneda, baby!” This makes composition of cospans by pushout well defined on isomorphism classes.
• Colimits are where generative effects live: an observation that fails to preserve colimits sees more in the whole than in the parts. Colimits of network diagrams describe connection (7 Sketches Chapter 6: “colimits and connection”).

JuliaLeanHaskell

Docs: FinSets · Limits & colimits · Free diagrams · Graphs — Kittenlab Lecture 9, Lecture 15

using Catlab
# colimits in FinSet: coproduct, pushout, coequalizer
coproduct(FinSet(2), FinSet(3)) |> apex        # FinSet(5)
f = FinFunction([1, 2], 3); g = FinFunction([1, 1], 2)
P = pushout(f, g); apex(P)                     # glue 1~1, 2~1 in the two codomains
coequalizer(FinFunction([1], 3), FinFunction([2], 3)) |> apex   # squish 1 and 2: FinSet(2)
# colimits of graphs are computed the same way, pointwise
G = path_graph(Graph, 3); H = cycle_graph(Graph, 3)
colimit(Span(id(G), id(G))) |> apex == G      # (up to iso) pushout along identities

#check CategoryTheory.Limits.colimit
#check CategoryTheory.Limits.IsColimit
#check CategoryTheory.Limits.colimit.ι       -- the coprojections (legs)
#check CategoryTheory.Limits.colimit.desc    -- the unique map out of the colimit
#check CategoryTheory.Limits.colimConstAdj   -- colim ⊣ const
#check CategoryTheory.Limits.Types.Quot      -- colimits in Type are quotients of disjoint unions

-- colimits in Hask of finite diagrams: a disjoint union modulo generated equivalence
-- e.g. the pushout of f :: z -> x and g :: z -> y on finite carriers, via representatives:
pushoutSet :: (Eq x, Eq y) => [x] -> [y] -> [z] -> (z -> x) -> (z -> y) -> [[Either x y]]
pushoutSet xs ys zs f g = classes
  where pairs   = [ (Left (f z), Right (g z)) | z <- zs ]
        elems   = map Left xs ++ map Right ys
        related a b = a == b || (a, b) `elem` pairs || (b, a) `elem` pairs
        closure a = [ b | b <- elems, reach a b ]
        reach a b = a == b || any (\c -> related a c && reach' c b [a]) elems
        reach' c b seen = c == b || any (\d -> related c d && not (d `elem` seen) && reach' d b (c:seen)) elems
        classes = foldr (\e acc -> if any (e `elem`) acc then acc else closure e : acc) [] elems