Finite Colimits in Set

theorem proof example

Definition 6.30. A category $\mathcal{C}$ has finite colimits if ${\mathrm{colim}}_{\mathcal{J}}D$ exists for every finite category $\mathcal{J}$ (finitely many morphisms, hence objects) and diagram $D:\mathcal{J}\to \mathcal{C}$.

Proposition 6.32. The following are equivalent: (1) $\mathcal{C}$ has all finite colimits; (2) $\mathcal{C}$ has an Initial Object and all pushouts; (3) $\mathcal{C}$ has all coequalizers and finite coproducts. (Proof idea: build any finite diagram inductively from these building blocks — e.g. the colimit of $A\to B\to Z$, $A\to C$, $A\to D$… is a pushout of pushouts, Example 6.33, 7S Exercise 6.35; [Bor94, Prop 2.8.2].)

Corollary 6.36. $\mathbf{FinSet}$ and $\mathbf{Set}$ have all finite colimits.

Theorem 6.37 (formula). Let $\mathcal{J}$ be presented by a finite graph $(V,A,s,t)$ with equations and $D:\mathcal{J}\to \mathbf{Set}$. Then

$${\mathrm{colim}}_{\mathcal{J}}D:=\{(v,d)\mid v\in V,d\in D(v)\}/\sim$$

where $\sim$ is the Equivalence Relation generated by $(v,d)\sim (w,e)$ whenever there is $a:v\to w$ with $D(a)(d)=e$, together with ${\iota }_v:D(v)\to \mathrm{colim}D$ sending $d$ to its class, is a colimit of $D$. “Whereas a finite limit is a subset of a product, a finite colimit is a quotient of a coproduct” — dual to Finite Limits in Set.

Sources: 7 Sketches §6.2.4 (Definition 6.30, Examples 6.31, 6.33, 6.38–6.42, Proposition 6.32, Corollary 6.36, Theorem 6.37, Exercises 6.35, 6.41); Kittenlab Lecture 9; CTfS §2.6 (Definitions 2.6.2.1, 2.6.3.1, Example 2.6.2.2, Exercises 2.6.2.4–2.6.2.7, 2.6.3.2)

Instances. Empty graph: $\varnothing$, the initial object (Example 6.38). Two vertices: $X\bigsqcup Y$ (Example 6.39). One vertex: $D(v)$ itself (Example 6.40). Span $X\stackrel{f}{\leftarrow }N\stackrel{g}{\to }Y$: $(X\bigsqcup Y)/(f(n)\sim g(n))$, the pushout (7S Exercise 6.41; the copy of $N$ is redundant since every $n$ is identified with $f(n)$). Parallel pair $f,g:X\rightrightarrows Y$: $Y/(f(x)\sim g(x))$, the coequalizer (Example 6.42) — the terminals of an interconnected circuit. CTfS instances: with $W=\varnothing$ the pushout is the coproduct; with $W=\mathbb{N}$, $X=\mathbb{Z}$, $f(w)=-(w+1)$ and $g$ the map to a point, the pushout $\mathbb{Z}{\bigsqcup }_{\mathbb{N}}\{\star \}$ collapses all negative integers to one point and keeps $0,1,2,\dots$ (CTfS Exercise 2.6.2.6); the coequalizer of $x\mapsto x$ and $x\mapsto x+1$ on $\mathbb{R}$ is a circle (CTfS Exercise 2.6.3.2). 7 Sketches Example 6.29: with $f(a)=\lfloor a/2\rfloor$, $g(a)=\lfloor (a+1)/2\rfloor$ on $\mathbb{N}$, the pushout is a single point, since $0\sim 0^{\prime }\sim 1\sim 1^{\prime }\sim \cdots$ by induction.

JuliaLeanHaskell

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

# Theorem 6.37 with union-find: colimit of a finite diagram in FinSet
using DataStructures
function set_colimit(sets::Vector{Int}, arrows::Vector{Tuple{Int,Int,Vector{Int}}})   # (v, w, D(a))
  offs = cumsum([0; sets[1:end-1]])                 # (v, d) ↦ offs[v] + d in the disjoint union
  uf = IntDisjointSets(sum(sets))
  for (v, w, Da) in arrows, d in 1:sets[v]
    union!(uf, offs[v] + d, offs[w] + Da[d])
  end
  roots = unique([find_root!(uf, i) for i in 1:sum(sets)])
  (length(roots), [Dict(d => findfirst(==(find_root!(uf, offs[v] + d)), roots) for d in 1:sets[v]) for v in eachindex(sets)])
end
set_colimit([4, 5, 3], [(1, 2, [1, 3, 5, 5]), (1, 3, [1, 1, 2, 3])])   # Exercise 6.26: pushout has 4 elements

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab
using Catlab
colimit(Span(FinFunction([1, 3, 5, 5], 5), FinFunction([1, 1, 2, 3], 3))) |> apex   # FinSet(4)

#check CategoryTheory.Limits.Types.Quot          -- colimits in Type as quotients of sigma types
#check CategoryTheory.Limits.HasFiniteColimits
#check CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts   -- Proposition 6.32 (2 ⇒ 1)
#check CategoryTheory.Limits.hasColimitsOfShape_of_hasCoequalizers_and_coproducts

-- colimit of a finite diagram on finite carriers: tag by vertex, then quotient by the generated relation
data Tagged a = Tagged Int a deriving (Eq, Show)
-- generated equivalence: pairs (Tagged v d, Tagged w (f d)) for each arrow; take connected components