Pushout

definition example theorem program

The pushout of a Span $X\stackrel{g}{\leftarrow }Z\stackrel{f}{\to }Y$ is its Colimit: an object $X{+}_{Z}Y$ with maps ${\iota }_X:X\to X{+}_{Z}Y$, ${\iota }_Y:Y\to X{+}_{Z}Y$ (and ${\iota }_Z={\iota }_X\circ g={\iota }_Y\circ f$) making the square commute, such that for any $W$ with ${\iota }_X^{\prime },{\iota }_Y^{\prime }$ commuting there is a unique $p_W:X{+}_{Z}Y\to W$ with $p_W\circ {\iota }_X={\iota }_X^{\prime }$, $p_W\circ {\iota }_Y={\iota }_Y^{\prime }$. ”$X{+}_{Z}Y$ is the Coproduct of $X$ and $Y$ but with the image of $Z$ in $X$ equalized by fiat with the image of $Z$ in $Y$.”

Sources: Kittenlab Lecture 9 (“Pushouts”, union-find implementation), 15 (composition of cospans by pushout, well-definedness up to iso); 7 Sketches §6.2.3 (Definition 6.13, Examples 6.14–6.18, Exercises 6.15, 6.17), §1.4.2 (pushing out a surjection); DaoFP §9.5 (colimits); CTfS §2.6.2 (Definition 2.6.2.1, Examples 2.6.2.2–2.6.2.3, Exercises 2.6.2.4–2.6.2.7, Lemma 2.6.2.8), Examples 4.5.3.28–4.5.3.29

In $\mathbf{Set}$ (Kittenlab)

$X{+}_{Z}Y=(X+Y)/\sim$ where $\sim$ is the Equivalence Relation generated by $f(z)\sim g(z)$ for all $z\in Z$. The universal property holds because “by the commutation property, all elements of each equivalence class have to go to the same element of $W$“. Implementation: put $X$ and $Y$ side by side in a union-find on $n+m$ elements, union! the pairs $(g(z),n+f(z))$, and read off roots. The same works for graphs and any C-Set: glue vertices and edges separately — “take two graphs, take their coproduct, and glue some of their edges and vertices together according to maps out of a third graph”.

Gluing and equating (Category Theory for Scientists)

“If one wishes to take two things and glue them together, with $A$ as the glue and $B$ and $C$ as the two things to be glued, the union is the pushout $B{\bigsqcup }_{A}C$.” Examples: $[0,1]{\bigsqcup }_{\{1\}}[1,2]=[0,2]$; “a cell in the torso or arm” glues the torso and the arm along the shoulder so shoulder cells are not double-counted; pushing “a college course” out along “a mathematics course $\mapsto$ an utterance of too hard” makes all math courses one and the same thing — “the power to equate different things can be exercised with pushouts” (CTfS Example 2.6.2.3); collapsing the boundary circle of a disk gives a sphere (CTfS Example 4.5.3.29). With $W=\varnothing$ the pushout is the coproduct, and pushing out the two projections of a relation $R\rightrightarrows X$ gives $X$ modulo the equivalence relation generated by $R$ (CTfS Exercise 2.6.2.7).

As a representable

Let $\mathsf{D}$ be the category $\bullet \leftarrow \bullet \to \bullet$. The pushout of $F:\mathsf{D}\to \mathcal{C}$ is a representing object for ${\mathrm{Hom}}_{{\mathcal{C}}^{\mathsf{D}}}(F,\Delta (-))$: a natural transformation $F\Rightarrow \Delta (W)$ is three morphisms, and naturality is exactly the commuting square; feeding the identity of the representing object into the isomorphism gives the cocone ${\iota }_X,{\iota }_Y,{\iota }_Z$, and naturality gives the factorization property (Kittenlab Lecture 9). Since isomorphic diagrams have isomorphic representing objects, pushouts are well defined on isomorphism classes of spans — used to show that composition of cospans is well defined (Lecture 15).

Uses

• Composition in the cospan category $\mathrm{Csp}(\mathcal{C})$ and in hypergraph categories / decorated cospans (7 Sketches Chapter 6: gluing circuits along shared terminals); open graphs.
• Pushing forward a Partition along a function (7 Sketches §1.4.2).
• Any finite colimit is built from coproducts and pushouts / coequalizers (7 Sketches §6.2.4). Dual: Pullback.

In compilers and databases

Graph rewriting is two pushouts: a pushout complement deletes the matched pattern and an ordinary pushout glues in the replacement (Double-Pushout Rewriting).

JuliaLeanHaskell

Docs: FinSets · Limits & colimits · C-set morphisms · ACSets API · Graphs — Kittenlab Lecture 9

# Kittenlab Lecture 9: pushout of finite sets via union-find
struct UnionFind; parent::Vector{Int}; UnionFind(n) = new(collect(1:n)); end
find_root(uf, i) = uf.parent[i] == i ? i : find_root(uf, uf.parent[i])
union!(uf, i, j) = (uf.parent[find_root(uf, j)] = find_root(uf, i))
function pushout_sets(f::Vector{Int}, g::Vector{Int}, n::Int, m::Int)   # f: Z → {1..n}, g: Z → {1..m}
  po = UnionFind(n + m)
  for z in eachindex(f); union!(po, f[z], n + g[z]); end
  roots = unique!([find_root(po, i) for i in 1:(n + m)])
  (Set(roots), Dict(i => find_root(po, i) for i in 1:n), Dict(j => find_root(po, n + j) for j in 1:m))
end
pushout_sets([1, 2], [1, 1], 3, 2)      # glue x1~y1, x2~y1: three classes

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

# Catlab
using Catlab
f = FinFunction([1, 2], 3); g = FinFunction([1, 1], 2)
P = pushout(f, g); apex(P), legs(P)
# graphs: glue two path graphs at an endpoint
G = path_graph(Graph, 3)
pt = @acset Graph begin V = 1 end
a = ACSetTransformation(pt, G; V = [3]); b = ACSetTransformation(pt, G; V = [1])
apex(pushout(a, b))                     # a path graph on 5 vertices

#check CategoryTheory.Limits.pushout        -- pushout f g with pushout.inl, pushout.inr, pushout.desc
#check CategoryTheory.Limits.pushout.condition
#check CategoryTheory.Limits.Types.pushoutCocone  -- a quotient of the sum

-- pushout of finite sets: disjoint union modulo generated equivalence (see Colimit for a generic version)
-- gluing two lists at their endpoints:
gluePaths :: [a] -> [a] -> [a]
gluePaths xs ys = xs ++ tail ys      -- identifies last xs with head ys