nLab final pullback complement

Final pullback complements

Final pullback complements


A final pullback complement is a “universal completion of a pair of arrows to a pullback”. Intuitively, it is a way to “remove part of an object of a category” while retaining information about how that part is “connected” to other parts. Final pullback complements play an important role in some kinds of span rewriting.


Given morphisms m:CAm:C\to A and g:ADg:A\to D in a category, a pullback complement is a pair of arrows f:CBf:C\to B and n:BDn:B\to D such that the square

C A B D \array{ C & \to & A \\ \downarrow & & \downarrow \\ B & \to & D }

commutes and is a pullback. This is of course the dual of a pushout complement.

A morphism of pullback complements is a map BBB\to B' making the obvious diagrams commute. A final pullback complement is a terminal object in the category of pullback complements. Since they have a universal property, final pullback complements are unique up to unique isomorphism when they exist.

Relation to exponentials

Recall from distributivity pullback that a pullback around (g,m)(g,m) is a diagram

X p C m A q g Y r D\array{ X & \xrightarrow{p} & C & \xrightarrow{m} & A\\ ^q\downarrow &&&& \downarrow^g\\ Y && \xrightarrow{r} && D}

in which the outer rectangle is a pullback, and that a distributivity pullback around (g,m)(g,m) is a terminal object in the category of pullbacks aroung (g,m)(g,m). This makes the following evident:


If a distributivity pullback around (g,m)(g,m) exists and has the property that pp is an isomorphism, then it is also a final pullback complement.

A distributivity pullback has precisely the universal property of an exponential object of mm along gg. Thus, whenever such an exponential Π gm\Pi_g m exists and the counit g *Π gmmg^* \Pi_g m \to m is an isomorphism, a final pullback complement exists. This is the case in particular in a locally cartesian closed category if gg and mm are both monomorphisms.

Relation to pushout complements

In an adhesive category, any pushout complement of a monomorphism is also a final pullback complement.


  • Andrea Corradini, Tobias Heindel, Frank Hermann, and Barbara König, Sesqui-pushout rewriting, 2006, springerlink, pdf.

Last revised on July 29, 2023 at 13:44:39. See the history of this page for a list of all contributions to it.