Pullback

definition example theorem

The pullback of a Cospan $X\stackrel{f}{\to }A\stackrel{g}{\leftarrow }Y$ is its Limit: an object $X{\times }_{A}Y$ with projections $c_x:X{\times }_{A}Y\to X$, $c_y:X{\times }_{A}Y\to Y$ such that $c_x;f=c_y;g$, universal among such squares. The diagonal leg $c_a$ of the cone is superfluous (it equals $c_x;f$), so pullback squares are drawn without it, marked with a corner symbol $┘$.

Sources: 7 Sketches Example 3.99, Remark 3.100, §7.2.1 (pullbacks in a topos), Definition 3.68 (the other “pullback”: ${\Delta }_F$); Kittenlab Lecture 13 (“typed products” = products in a Slice Category), 14 (pullback of subsets); DaoFP §11.2 (“Pullbacks”, “Substitution”, “Base-change functor”); CTfS §2.5.1 (Definition 2.5.1.1, Examples 2.5.1.8–2.5.1.10, Lemma 2.5.1.14, Proposition 2.5.1.17, Exercises 2.5.1.2–2.5.1.19)

• In $\mathbf{Set}$: $X{\times }_{A}Y=\{(x,y)\mid f(x)=g(y)\}$ (Finite Limits in Set). Example 3.99: $X=\underline{6}$, $Y=\underline{4}$, $A=\{\mathsf{red},\mathsf{blue},\mathsf{black}\}$: the pullback selects pairs $(i,j)$ with the same colour. Pullbacks are how $\Pi$-queries “pair and select data” (database join).
• Defining new concepts in ologs (CTfS §2.5.1.7). A fiber product defines a type from old ones, which “reduces the chance of misunderstandings between different groups of people”: “a customer that is wealthy and loyal” is the pullback of “a wealthy customer” and “a loyal customer” over “a customer” — and naming that box “a good customer” is a definition. “A person whose favourite colour is blue” and “a dog whose owner is a woman” are honest pullback labels; calling the pullback of “a space in our house” and “a piece of furniture” over “a width” a good fit is misleading, since equal width is not fit (CTfS Exercise 2.5.1.10). Two chained pullbacks define “a cellphone that has a bad battery” as “a cellphone that has a battery which remains charged for less than one hour” — justified by the Pasting Lemma for Pullbacks. Colouring a 5-element and a 3-element set red/blue/yellow, the pullback over the colours sits inside the $5\times 3$ grid as the cells whose row and column have the same colour (CTfS Exercise 2.5.1.3).
• Typed products (Kittenlab): the product in $\mathbf{FinSet}/T$ of $(A,t)$ and $(A^{\prime },t^{\prime })$ is the pullback $A{\times }_T{A}^{\prime }$ — pairs of elements of the same type. Pullback of a subset $\chi :Y\to \mathbb{B}$ along $f:X\to Y$ is $\chi \circ f$, the preimage; in the subobject picture this is literally a categorical pullback of $U\hookrightarrow Y$ along $f$ (Direct Image, Preimage, and Dual Image).
• Base change / substitution (DaoFP §11.2): pulling back a family $p:e\to c$ (a Dependent Type) along $f:c^{\prime }\to c$ gives the family $f^{\ast }e\to c^{\prime }$ — substituting $f$ into the type; $f^{\ast }:\mathcal{C}/c\to \mathcal{C}/c^{\prime }$ is the base-change functor, with adjoints ${\Sigma }_f$ $⊣f^{\ast }⊣$ ${\Pi }_f$.
• Monos are pullback-stable; in a Topos every mono is a pullback of $\mathsf{true}:1\to \Omega$ (Subobject Classifier). Pullback of a covering gives restriction. The pullback along a functor ${\Delta }_F$ is, via the Category of Elements, a pullback in $\mathbf{Cat}$ (Remark 3.100).
• Dual: Pushout.

JuliaLeanHaskell

Docs: FinSets · Limits & colimits — Kittenlab Lecture 13

using Catlab
f = FinFunction([1, 2, 2, 3, 1, 3], 3)      # colours of 6 things
g = FinFunction([1, 1, 3, 2], 3)            # colours of 4 things
P = pullback(f, g)
apex(P)                                     # FinSet(8): pairs with equal colour
collect(zip(collect(legs(P)[1]), collect(legs(P)[2])))
# pullback of graphs / ACSets works the same way (pointwise)

#check CategoryTheory.Limits.pullback        -- pullback f g with pullback.fst, pullback.snd, pullback.lift
#check CategoryTheory.Limits.pullback.condition   -- fst ≫ f = snd ≫ g
#check CategoryTheory.Limits.Types.pullbackIsoPullback   -- in Type: { p : X × Y // f p.1 = g p.2 }
#check CategoryTheory.Over.pullback           -- base change C/c ⥤ C/c'

-- the pullback in Hask as a subtype of the product (on finite carriers)
pullbackSet :: Eq c => [a] -> [b] -> (a -> c) -> (b -> c) -> [(a, b)]
pullbackSet as bs f g = [ (a, b) | a <- as, b <- bs, f a == g b ]
 
-- base change of a "family" p :: e -> c along f :: c' -> c: pairs (c', e) with f c' = p e