Constructing pullbacks from binary products and equalizers
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.
Equations
- category_theory.limits.has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair f g = let π₁ : X ⨯ Y ⟶ X := category_theory.limits.prod.fst, π₂ : X ⨯ Y ⟶ Y := category_theory.limits.prod.snd, e : category_theory.limits.equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := category_theory.limits.equalizer.ι (π₁ ≫ f) (π₂ ≫ g) in {cone := category_theory.limits.pullback_cone.mk (e ≫ π₁) (e ≫ π₂) _, is_limit := category_theory.limits.pullback_cone.is_limit.mk (e ≫ π₁) (e ≫ π₂) _ (λ (s : category_theory.limits.pullback_cone f g), category_theory.limits.equalizer.lift (category_theory.limits.prod.lift (s.π.app category_theory.limits.walking_cospan.left) (s.π.app category_theory.limits.walking_cospan.right)) _) _ _ _}
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.
Equations
- category_theory.limits.has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair f g = let ι₁ : Y ⟶ Y ⨿ Z := category_theory.limits.coprod.inl, ι₂ : Z ⟶ Y ⨿ Z := category_theory.limits.coprod.inr, c : Y ⨿ Z ⟶ category_theory.limits.coequalizer (f ≫ ι₁) (g ≫ ι₂) := category_theory.limits.coequalizer.π (f ≫ ι₁) (g ≫ ι₂) in {cocone := category_theory.limits.pushout_cocone.mk (ι₁ ≫ c) (ι₂ ≫ c) _, is_colimit := category_theory.limits.pushout_cocone.is_colimit.mk (ι₁ ≫ c) (ι₂ ≫ c) _ (λ (s : category_theory.limits.pushout_cocone f g), category_theory.limits.coequalizer.desc (category_theory.limits.coprod.desc (s.ι.app category_theory.limits.walking_span.left) (s.ι.app category_theory.limits.walking_span.right)) _) _ _ _}
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.