Constructing pullbacks from binary products and equalizers

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

theorem CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [𝒞 : Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (pair X Y)] [HasLimit (parallelPair (CategoryStruct.comp prod.fst f) (CategoryStruct.comp prod.snd g))] : HasLimit (cospan f g)

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.

theorem CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers (C : Type u) [Category.{v, u} C] [HasBinaryProducts C] [HasEqualizers C] : HasPullbacks C

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.

theorem CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair {C : Type u} [𝒞 : Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasColimit (pair Y Z)] [HasColimit (parallelPair (CategoryStruct.comp f coprod.inl) (CategoryStruct.comp g coprod.inr))] : HasColimit (span f g)

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.

theorem CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers (C : Type u) [Category.{v, u} C] [HasBinaryCoproducts C] [HasCoequalizers C] : HasPushouts C

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.