Constructing binary product from pullbacks and terminal object.

The product is the pullback over the terminal objects. In particular, if a category has pullbacks and a terminal object, then it has binary products.

We also provide the dual.

def isBinaryProductOfIsTerminalIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (c : CategoryTheory.Limits.Cone F) {X : C} (hX : CategoryTheory.Limits.IsTerminal X) (f : F.toPrefunctor.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ X) (g : F.toPrefunctor.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ X) (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (c.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (c.π.app { as := CategoryTheory.Limits.WalkingPair.right }) (_ : CategoryTheory.CategoryStruct.comp (c.π.app { as := CategoryTheory.Limits.WalkingPair.left }) f = CategoryTheory.CategoryStruct.comp (c.π.app { as := CategoryTheory.Limits.WalkingPair.right }) g))) : CategoryTheory.Limits.IsLimit c

If a span is the pullback span over the terminal object, then it is a binary product.

Equations

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

def isProductOfIsTerminalIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsTerminal Z) (H₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k (_ : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g))) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)

The pullback over the terminal object is the product

Equations

• isProductOfIsTerminalIsPullback f g h k H₁ H₂ = isBinaryProductOfIsTerminalIsPullback (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryFan.mk h k) H₁ f g H₂

def isPullbackOfIsTerminalIsProduct {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsTerminal Z) (H₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k (_ : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g))

The product is the pullback over the terminal object.

Equations

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

noncomputable def limitConeOfTerminalAndPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : CategoryTheory.Limits.LimitCone F

Any category with pullbacks and a terminal object has a limit cone for each walking pair.

Equations

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

theorem hasBinaryProducts_of_hasTerminal_and_pullbacks (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasBinaryProducts C

Any category with pullbacks and terminal object has binary products.

noncomputable def preservesBinaryProductsOfPreservesTerminalAndPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

A functor that preserves terminal objects and pullbacks preserves binary products.

Equations

• preservesBinaryProductsOfPreservesTerminalAndPullbacks F = CategoryTheory.Limits.PreservesLimitsOfShape.mk

noncomputable def prodIsoPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : X ⨯ Y ≅ CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)

In a category with a terminal object and pullbacks, a product of objects X and Y is isomorphic to a pullback.

Equations

• prodIsoPullback X Y = CategoryTheory.Limits.limit.isoLimitCone (limitConeOfTerminalAndPullbacks (CategoryTheory.Limits.pair X Y))

def isBinaryCoproductOfIsInitialIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (c : CategoryTheory.Limits.Cocone F) {X : C} (hX : CategoryTheory.Limits.IsInitial X) (f : X ⟶ F.toPrefunctor.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : X ⟶ F.toPrefunctor.obj { as := CategoryTheory.Limits.WalkingPair.right }) (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (c.ι.app { as := CategoryTheory.Limits.WalkingPair.left }) (c.ι.app { as := CategoryTheory.Limits.WalkingPair.right }) (_ : CategoryTheory.CategoryStruct.comp f (c.ι.app { as := CategoryTheory.Limits.WalkingPair.left }) = CategoryTheory.CategoryStruct.comp g (c.ι.app { as := CategoryTheory.Limits.WalkingPair.right })))) : CategoryTheory.Limits.IsColimit c

If a cospan is the pushout cospan under the initial object, then it is a binary coproduct.

Equations

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

def isCoproductOfIsInitialIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsInitial W) (H₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g (_ : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)

The pushout under the initial object is the coproduct

Equations

• isCoproductOfIsInitialIsPushout f g h k H₁ H₂ = isBinaryCoproductOfIsInitialIsPushout (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryCofan.mk f g) H₁ h k H₂

def isPushoutOfIsInitialIsCoproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsInitial W) (H₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g (_ : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g))

The coproduct is the pushout under the initial object.

Equations

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

noncomputable def colimitCoconeOfInitialAndPushouts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : CategoryTheory.Limits.ColimitCocone F

Any category with pushouts and an initial object has a colimit cocone for each walking pair.

Equations

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

theorem hasBinaryCoproducts_of_hasInitial_and_pushouts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasBinaryCoproducts C

Any category with pushouts and initial object has binary coproducts.

noncomputable def preservesBinaryCoproductsOfPreservesInitialAndPushouts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

A functor that preserves initial objects and pushouts preserves binary coproducts.

Equations

• preservesBinaryCoproductsOfPreservesInitialAndPushouts F = CategoryTheory.Limits.PreservesColimitsOfShape.mk

noncomputable def coprodIsoPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⨿ Y ≅ CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)

In a category with an initial object and pushouts, a coproduct of objects X and Y is isomorphic to a pushout.

Equations

• coprodIsoPushout X Y = CategoryTheory.Limits.colimit.isoColimitCocone (colimitCoconeOfInitialAndPushouts (CategoryTheory.Limits.pair X Y))