Constructing equalizers from pullbacks and binary products.

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

TODO: generalize universe

@[reducible, inline]

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

Define the equalizing object

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Define the equalizing morphism

Equations

• One or more equations did not get rendered due to their size.

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

@[reducible, inline]

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

Define the equalizing cone

Equations

• One or more equations did not get rendered due to their size.

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

Show the equalizing cone is a limit

Equations

• One or more equations did not get rendered due to their size.

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

Any category with pullbacks and binary products, has equalizers.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Define the equalizing object

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Define the equalizing morphism

Equations

• One or more equations did not get rendered due to their size.

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

@[reducible, inline]

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

Define the equalizing cocone

Equations

• One or more equations did not get rendered due to their size.

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

Show the equalizing cocone is a colimit

Equations

• One or more equations did not get rendered due to their size.

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

Any category with pullbacks and binary products, has equalizers.

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

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

Equations

• One or more equations did not get rendered due to their size.