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

source

theorem category_theory.limits.has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair {C : Type u} [𝒞 : category_theory.category C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [category_theory.limits.has_limit (category_theory.limits.pair X Y)] [category_theory.limits.has_limit (category_theory.limits.parallel_pair (category_theory.limits.prod.fst ≫ f) (category_theory.limits.prod.snd ≫ g))] :

category_theory.limits.has_limit (category_theory.limits.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.

source

theorem category_theory.limits.has_pullbacks_of_has_binary_products_of_has_equalizers (C : Type u) [𝒞 : category_theory.category C] [category_theory.limits.has_binary_products C] [category_theory.limits.has_equalizers C] :

category_theory.limits.has_pullbacks 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.

source

theorem category_theory.limits.has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair {C : Type u} [𝒞 : category_theory.category C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [category_theory.limits.has_colimit (category_theory.limits.pair Y Z)] [category_theory.limits.has_colimit (category_theory.limits.parallel_pair (f ≫ category_theory.limits.coprod.inl) (g ≫ category_theory.limits.coprod.inr))] :

category_theory.limits.has_colimit (category_theory.limits.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.

source

theorem category_theory.limits.has_pushouts_of_has_binary_coproducts_of_has_coequalizers (C : Type u) [𝒞 : category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_coequalizers C] :

category_theory.limits.has_pushouts 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.