Pasting Lemma for Pullbacks

theorem proof

Proposition 7.3 (pasting lemma). In the commutative diagram below suppose the right square $(B,C,B^{\prime },C^{\prime })$ is a Pullback. Then the left square $(A,B,A^{\prime },B^{\prime })$ is a pullback if and only if the outer rectangle $(A,C,A^{\prime },C^{\prime })$ is a pullback.

This removes the ambiguity of the corner symbol $┘$ in a rectangle made of two squares: when the right square is a pullback, “the left square is a pullback” and “the whole rectangle is a pullback” mean the same thing.

Sources: 7 Sketches §7.2.1, Proposition 7.3, Exercise 7.4 (proof), Exercises 7.7–7.8 (applications: pullback of an iso is an iso, monos are pullback-stable); CTfS Proposition 2.5.1.17 (proof via elements $A{\times }_B(B{\times }_C{C}^{\prime })\cong A{\times }_C{C}^{\prime }$)

Proof (7S Exercise 7.4)

($\Rightarrow$) Suppose the left square is a pullback and let $(X,p:X\to C,q:X\to A^{\prime })$ satisfy $q;f^{\prime };g^{\prime }=p;h_3$. The right pullback gives a unique $r:X\to B$ with $r;h_2=q;f^{\prime }$ and $r;g=p$; then the left pullback gives a unique $r^{\prime }:X\to A$ with $r^{\prime };f=r$, $r^{\prime };h_1=q$. So $r^{\prime }$ mediates for the rectangle, and any other mediator $r_0$ must have $r_0;f=r$ (uniqueness for the right square) and then $r_0=r^{\prime }$ (uniqueness for the left square).

($\Leftarrow$) Suppose the rectangle is a pullback and $(X,r:X\to B,q:X\to A^{\prime })$ satisfies $r;h_2=q;f^{\prime }$. Put $p:=r;g$; then $p;h_3=q;f^{\prime };g^{\prime }$, so the rectangle gives a unique $r^{\prime }:X\to A$ with $r^{\prime };f;g=p$ and $r^{\prime };h_1=q$. Both $r^{\prime };f$ and $r$ satisfy the two equations characterizing the mediator into the right pullback, so $r^{\prime };f=r$. Uniqueness of $r^{\prime }$ follows from uniqueness for the rectangle. $■$

In ologs (Category Theory for Scientists)

CTfS proves the set version by elements — $(a,b,(b,c,c^{\prime }))\mapsto (a,c,c^{\prime })$ is a bijection $A{\times }_B(B{\times }_C{C}^{\prime })\cong A{\times }_C{C}^{\prime }$ — and uses it to unfold definitions: if “a cellphone that has a bad battery” is the pullback of “a cellphone $\stackrel{\text{has}}{\to }$ a battery” along “a bad battery $\to$ a battery”, and “a bad battery” is itself the pullback of “a battery $\stackrel{\text{remains charged for}}{\to }$ a duration” along “less than 1 hour $\to$ a duration”, then “a cellphone that has a bad battery” is “a cellphone that has a battery which remains charged for less than one hour”.

Consequences

• The pullback of an Isomorphism is an isomorphism, and $(A,B,A,B)$ with identities and $f$ twice is a pullback (7S Exercise 7.7).
• Monos are stable under pullback (7S Exercise 7.8): two applications of the lemma to a cube.

JuliaLean

Docs: FinSets · Limits & colimits

using Catlab
# pasting in FinSet: pulling back in two steps equals pulling back along the composite
g′ = FinFunction([1, 2, 2], 3)          # B' → C'
h3 = FinFunction([1, 3, 3, 2], 3)       # C  → C'
f′ = FinFunction([1, 1, 2], 3)          # A' → B'
right = pullback(g′, h3)                # B := B' ×_{C'} C, with h2 : B → B'
h2 = legs(right)[1]
left = pullback(f′, h2)                 # A := A' ×_{B'} B
outer = pullback(f′ ⋅ g′, h3)           # A' ×_{C'} C
ob(left) == ob(outer)                   # true: FinSet(3) both ways

import Mathlib
open CategoryTheory Limits
#check @CategoryTheory.Limits.bigSquareIsPullback   -- left ∧ right pullbacks ⇒ rectangle
#check @CategoryTheory.Limits.leftSquareIsPullback  -- rectangle ∧ right ⇒ left
#check @CategoryTheory.IsPullback.paste_horiz
#check @CategoryTheory.IsPullback.of_right          -- cancellation form