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
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 April 26, 2023 at 16:30:41. See the history of this page for a list of all contributions to it.