nLab
pushout complement

Idea

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.

Definition

Given morphisms $m:C\to A$ and $g:A\to D$ in a category, a pushout complement is a pair of arrows $f:C\to B$ and $n:B\to D$ such that the square

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

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 $m$ 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.

Examples

• In the category Set, if $m$ and $g$ are injections then a pushout complement always exists: take $B = D \setminus (A\setminus C)$.

• In a coherent category, if $C=\emptyset$ and $g$ is a monomorphism, then a pushout complement is the same as an ordinary complement for the subobject $A\to D$.

• 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.

References

• H. Ehrig, M. Pfender, and H.J. Schneider. Graph-grammars: an algebraic approach. In IEEE Conf. on Automata and Switching Theory, pages 167–180, 1973.

• Steve Lack and Pawel Sobocinski, Adhesive categories, PDF