Constructing equalizers from pullbacks and binary products.

If a category has pullbacks and binary products, then it has equalizers.

TODO: generalize universe

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] [HasPullbacks C] (F : Functor WalkingParallelPair C) : C

Define the equalizing object

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] [HasPullbacks C] (F : Functor WalkingParallelPair C) : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero

Define the equalizing morphism

theorem CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] [HasPullbacks C] (F : Functor WalkingParallelPair C) : pullbackFst F = pullback.snd (prod.lift (CategoryStruct.id (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) (prod.lift (CategoryStruct.id (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] [HasPullbacks C] (F : Functor WalkingParallelPair C) : Cone F

Define the equalizing cone

noncomputable def CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] [HasPullbacks C] (F : Functor WalkingParallelPair C) : IsLimit (equalizerCone F)

Show the equalizing cone is a limit

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

Any category with pullbacks and binary products, has equalizers.

theorem CategoryTheory.Limits.preservesEqualizers_of_preservesPullbacks_and_binaryProducts {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (G : Functor C D) [HasBinaryProducts C] [HasPullbacks C] [PreservesLimitsOfShape (Discrete WalkingPair) G] [PreservesLimitsOfShape WalkingCospan G] : PreservesLimitsOfShape WalkingParallelPair G

A functor that preserves pullbacks and binary products also preserves equalizers.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasPushouts C] (F : Functor WalkingParallelPair C) : C

Define the equalizing object

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasPushouts C] (F : Functor WalkingParallelPair C) : F.obj WalkingParallelPair.one ⟶ constructCoequalizer F

Define the equalizing morphism

theorem CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasPushouts C] (F : Functor WalkingParallelPair C) : pushoutInl F = pushout.inr (coprod.desc (CategoryStruct.id (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left)) (coprod.desc (CategoryStruct.id (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasPushouts C] (F : Functor WalkingParallelPair C) : Cocone F

Define the equalizing cocone

noncomputable def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasPushouts C] (F : Functor WalkingParallelPair C) : IsColimit (coequalizerCocone F)

Show the equalizing cocone is a colimit

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

Any category with pullbacks and binary products, has equalizers.

theorem CategoryTheory.Limits.preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (G : Functor C D) [HasBinaryCoproducts C] [HasPushouts C] [PreservesColimitsOfShape (Discrete WalkingPair) G] [PreservesColimitsOfShape WalkingSpan G] : PreservesColimitsOfShape WalkingParallelPair G

A functor that preserves pushouts and binary coproducts also preserves coequalizers.