mathlib documentation

category_theory.limits.constructions.binary_products

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 is_product_of_is_terminal_is_pullback {C : Type u} [category_theory.category C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : category_theory.limits.is_terminal Z) (H₂ : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k _)) :

category_theory.limits.is_limit (category_theory.limits.binary_fan.mk h k)

The pullback over the terminal object is the product

Equations

is_product_of_is_terminal_is_pullback f g h k H₁ H₂ = {lift := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)), H₂.lift (category_theory.limits.pullback_cone.mk (c.π.app category_theory.limits.walking_pair.left) (c.π.app category_theory.limits.walking_pair.right) _), fac' := _, uniq' := _}

def is_pullback_of_is_terminal_is_product {C : Type u} [category_theory.category C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : category_theory.limits.is_terminal Z) (H₂ : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk h k)) :

category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k _)

The product is the pullback over the terminal object.

Equations

is_pullback_of_is_terminal_is_product f g h k H₁ H₂ = (category_theory.limits.pullback_cone.mk h k _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨H₂.lift (category_theory.limits.binary_fan.mk s.fst s.snd), _⟩)

theorem has_binary_products_of_terminal_and_pullbacks (C : Type u) [category_theory.category C] [category_theory.limits.has_terminal C] [category_theory.limits.has_pullbacks C] :

category_theory.limits.has_binary_products C

Any category with pullbacks and terminal object has binary products.

def is_coproduct_of_is_initial_is_pushout {C : Type u} [category_theory.category C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : category_theory.limits.is_initial W) (H₂ : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk f g _)) :

category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk f g)

The pushout under the initial object is the coproduct

Equations

is_coproduct_of_is_initial_is_pushout f g h k H₁ H₂ = {desc := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)), H₂.desc (category_theory.limits.pushout_cocone.mk (c.ι.app category_theory.limits.walking_pair.left) (c.ι.app category_theory.limits.walking_pair.right) _), fac' := _, uniq' := _}

def is_pushout_of_is_initial_is_coproduct {C : Type u} [category_theory.category C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : category_theory.limits.is_terminal Z) (H₂ : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk h k)) :

category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k _)

The coproduct is the pushout under the initial object.

Equations

is_pushout_of_is_initial_is_coproduct f g h k H₁ H₂ = (category_theory.limits.pullback_cone.mk h k _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨H₂.lift (category_theory.limits.binary_fan.mk s.fst s.snd), _⟩)

theorem has_binary_coproducts_of_initial_and_pushouts (C : Type u) [category_theory.category C] [category_theory.limits.has_initial C] [category_theory.limits.has_pushouts C] :

category_theory.limits.has_binary_coproducts C

Any category with pushouts and initial object has binary coproducts.