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.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ X) (g : F.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.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 X Y 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.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 X Y 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 ⋯)

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.

theorem preservesBinaryProducts_of_preservesTerminal_and_pullbacks {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.

noncomputable def prodIsoPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X 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))

@[simp]

theorem prodIsoPullback_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) = CategoryTheory.Limits.prod.fst

@[simp]

theorem prodIsoPullback_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h

@[simp]

theorem prodIsoPullback_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) = CategoryTheory.Limits.prod.snd

@[simp]

theorem prodIsoPullback_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h

@[simp]

theorem prodIsoPullback_inv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)

@[simp]

theorem prodIsoPullback_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h

@[simp]

theorem prodIsoPullback_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)

@[simp]

theorem prodIsoPullback_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h

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.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : X ⟶ F.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.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 X Y 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.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 X Y 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 ⋯)

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.

theorem preservesBinaryCoproducts_of_preservesInitial_and_pushouts {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.

noncomputable def coprodIsoPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X 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))

@[simp]

theorem inl_coprodIsoPushout_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)

@[simp]

theorem inl_coprodIsoPushout_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h

@[simp]

theorem inr_coprodIsoPushout_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)

@[simp]

theorem inr_coprodIsoPushout_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h

@[simp]

theorem inl_coprodIsoPushout_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inl

@[simp]

theorem inl_coprodIsoPushout_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h

@[simp]

theorem inr_coprodIsoPushout_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inr

@[simp]

theorem inr_coprodIsoPushout_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h