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 and in a category, a pullback complement is a pair of arrows and such that the square commutes and is a pullback. This is of course the dual of a pushout complement.
A morphism of pullback complements is a map 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.
Recall from distributivity pullback that a pullback around is a diagram
in which the outer rectangle is a pullback, and that a distributivity pullback around is a terminal object in the category of pullbacks aroung . This makes the following evident:
If a distributivity pullback around exists and has the property that is an isomorphism, then it is also a final pullback complement.
A distributivity pullback has precisely the universal property of an exponential object of along . Thus, whenever such an exponential exists and the counit is an isomorphism, a final pullback complement exists. This is the case in particular in a locally cartesian closed category if and are both monomorphisms.
In an adhesive category, any pushout complement of a monomorphism is also a final pullback complement.
Last revised on September 23, 2024 at 10:12:08. See the history of this page for a list of all contributions to it.