mathlib3 documentation

category_theory.limits.constructions.pullbacks

Constructing pullbacks from binary products and equalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If a category as binary products and equalizers, then it has pullbacks. Also, if a category has binary coproducts and coequalizers, then it has pushouts

If the product X ⨯ Y and the equalizer of π₁ ≫ f and π₂ ≫ g exist, then the pullback of f and g exists: It is given by composing the equalizer with the projections.

If a category has all binary products and all equalizers, then it also has all pullbacks. As usual, this is not an instance, since there may be a more direct way to construct pullbacks.

If the coproduct Y ⨿ Z and the coequalizer of f ≫ ι₁ and g ≫ ι₂ exist, then the pushout of f and g exists: It is given by composing the inclusions with the coequalizer.

If a category has all binary coproducts and all coequalizers, then it also has all pushouts. As usual, this is not an instance, since there may be a more direct way to construct pushouts.