Finite Limits in Set

theorem proof example program

Theorem 3.95. Let $\mathcal{J}$ be a category presented by a finite graph $(V,A,s,t)$ with equations, $V=\{v_1,\dots ,v_n\}$, and $D:\mathcal{J}\to \mathbf{Set}$. Then

$$\underset{\mathcal{J}}{\lim }D:=\{(d_1,\dots ,d_n)\mid d_i\in D(v_i)\text{ and }D(a)(d_i)=d_j\text{ for all }a:v_i\to v_j\in A\}$$

with projections $p_i(d_1,\dots ,d_n)=d_i$ is a Limit of $D$. “As far as limits are concerned, the equations in $\mathcal{J}$ don’t matter.”

Sources: 7 Sketches §3.5.3 (Theorem 3.95, Examples 3.96, 3.99, Exercises 3.97, 3.98); DaoFP §9.5 (limits in $\mathbf{Set}$ are cones with apex $1$); Kittenlab Lecture 13–14; CTfS §2.5 (Definition 2.5.1.1, Lemma 2.5.1.14, Proposition 2.5.1.17, Exercises 2.5.1.2–2.5.1.6, 2.5.3.5)

Instances

• Empty graph: $n=0$, one empty tuple $()$: the limit is $\{()\}$, the Terminal Object (Example 3.96).
• Two vertices, no arrows: pairs $(d_1,d_2)$, the Product $A\times B$ (7S Exercise 3.97).
• One vertex: $\lim D=D(v)$ itself (7S Exercise 3.98).
• Cospan $x\stackrel{f}{\to }a\stackrel{g}{\leftarrow }y$: triples $(d_x,d_a,d_y)$ with $f(d_x)=d_a=g(d_y)$, i.e. pairs $(d_x,d_y)$ with $f(d_x)=g(d_y)$: the Pullback $X{\times }_{A}Y$ (Example 3.99) — pairs $(i,j)\in \underline{6}\times \underline{4}$ whose colours agree.
• CTfS’s fiber product keeps the middle coordinate: $X{\times }_{Z}Y:=\{(x,w,y)\mid f(x)=w=g(y)\}$ — the same set up to isomorphism. Edge cases: if $Y=\varnothing$ the pullback is empty; if $Z$ is a point it is the product $X\times Y$ (CTfS Exercise 2.5.1.5). With Aristotelian space $S={\mathbb{R}}^3$ and time $T=\mathbb{R}$ and $X$ = “the center of mass of MIT at its founding”, pulling the projections of $S\times T$ back along the point gives the world-line through that place (all times) and the whole of space at that instant (CTfS Exercise 2.5.1.6).
• Parallel pair $f,g:a\rightrightarrows b$: $\{d\in D(a)\mid f(d)=g(d)\}$, the Equalizer — “solutions of a system of equations” (DaoFP).
• $!:\mathcal{C}\to \underline{1}$ on the email schema: tuples (email, address) with $sent\_by=received\_by=$ address, i.e. self-sent emails: ${\Pi }_{!}(I)$ (Data Migration Functor).

The formula “selects tuples satisfying equations or constraints — this is what allows us to express queries in terms of limits”. It is the special case of DaoFP’s description: an element of $\lim D$ is a cone with apex $1$, i.e. a compatible choice of one element per vertex. For colimits in $\mathbf{Set}$ the dual formula is a disjoint union modulo the Equivalence Relation generated by $d\sim D(a)(d)$ (7 Sketches §6.2.4).

JuliaLeanHaskell

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

# the tuple formula for a finite diagram in FinSet given by sets and generating functions
function set_limit(sets::Vector{Int}, arrows::Vector{Tuple{Int,Int,Vector{Int}}})   # (i, j, D(a))
  tuples = Iterators.product((1:n for n in sets)...)
  [t for t in tuples if all(Da[t[i]] == t[j] for (i, j, Da) in arrows)]
end
set_limit([4, 3, 2], [(1, 2, [1, 1, 2, 3]), (3, 2, [1, 3])])   # pullback: [(1,1,1), (2,1,1), (4,3,2)]

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

using Catlab
limit(Cospan(FinFunction([1, 1, 2, 3], 3), FinFunction([1, 3], 3))) |> apex   # FinSet(3)

#check CategoryTheory.Limits.Types.limitCone      -- limit in Type: { u : ∀ j, F.obj j // ∀ f, F.map f (u j) = u k }
#check CategoryTheory.Limits.Types.limitEquivSections

-- limit of a finite diagram in Hask on finite carriers: compatible tuples
data FinDiagram a = FinDiagram { carriers :: [[a]], arrows :: [(Int, Int, a -> a)] }
limitTuples :: Eq a => FinDiagram a -> [[a]]
limitTuples (FinDiagram cs as) = [ t | t <- sequence cs, and [ f (t !! i) == t !! j | (i, j, f) <- as ] ]