Equalizers as pullbacks of products

Also see CategoryTheory.Limits.Constructions.Equalizers for very similar results.

theorem CategoryTheory.Limits.isPullback_equalizer_prod {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] [HasBinaryProduct Y Y] : IsPullback (equalizer.ι f g) (CategoryStruct.comp (equalizer.ι f g) f) (prod.lift f g) (prod.lift (CategoryStruct.id Y) (CategoryStruct.id Y))

The equalizer of f g : X ⟶ Y is the pullback of the diagonal map Y ⟶ Y × Y along the map (f, g) : X ⟶ Y × Y.

theorem CategoryTheory.Limits.isPushout_coequalizer_coprod {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] [HasBinaryCoproduct X X] : IsPushout (coprod.desc f g) (coprod.desc (CategoryStruct.id X) (CategoryStruct.id X)) (coequalizer.π f g) (CategoryStruct.comp f (coequalizer.π f g))

The coequalizer of f g : X ⟶ Y is the pushout of the diagonal map X ⨿ X ⟶ X along the map (f, g) : X ⨿ X ⟶ Y.