A pushout complement is a “completion of a pair of arrows to a pushout”. 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. Pushout complements play an important role in some kinds of span rewriting.
Given morphisms and in a category, a pushout complement is a pair of arrows and such that the square commutes and is a pushout.
In general, even in good categories, pushout complements may not exist. However, if they do exist, then as long as the category is adhesive (such as a topos) and is a monomorphism, they are unique up to unique isomorphism. In the language of homotopy type theory, the type of such pushout complements is an h-proposition.
In the category Set, if and are injections then a pushout complement always exists: take .
In a coherent category, if and is a monomorphism, then a pushout complement is the same as an ordinary complement for the subobject .
In a category of graphs, pushout complements play an important role in double pushout graph rewriting.
The dual of a pushout complement is a pullback complement. Important pullback complements include final pullback complements, which arise from exponential objects of monomorphisms.
H. Ehrig, M. Pfender and H. J. Schneider. Graph-grammars: An algebraic approach, 14th Annual Symposium on Switching and Automata Theory, 1973, pp. 167-180. (doi:10.1109/SWAT.1973.11)
Steve Lack and Pawel Sobocinski, Adhesive categories, Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. doi:10.1007/978-3-540-24727-2_20, PDF
Last revised on July 22, 2025 at 12:26:33. See the history of this page for a list of all contributions to it.