pushout complement

Pushout complements


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 m:CAm:C\to A and g:ADg:A\to D in a category, a pushout 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 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 mm 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.