# mathlibdocumentation

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_binary_product_of_is_terminal_is_pullback {C : Type u} {X : C} (f : X) (g : X)  :

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

Equations
def is_product_of_is_terminal_is_pullback {C : Type u} {W X Y Z : C} (f : X Z) (g : Y Z) (h : W X) (k : W Y)  :

The pullback over the terminal object is the product

Equations
• H₁ H₂ =
def is_pullback_of_is_terminal_is_product {C : Type u} {W X Y Z : C} (f : X Z) (g : Y Z) (h : W X) (k : W Y)  :

The product is the pullback over the terminal object.

Equations
• H₁ H₂ = (λ (s : , , _⟩)

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

Equations

Any category with pullbacks and terminal object has binary products.

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

Equations
noncomputable def prod_iso_pullback {C : Type u} (X Y : C)  :

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

Equations
def is_binary_coproduct_of_is_initial_is_pushout {C : Type u} {X : C} (f : X ) (g : X )  :

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

Equations
def is_coproduct_of_is_initial_is_pushout {C : Type u} {W X Y Z : C} (f : X Z) (g : Y Z) (h : W X) (k : W Y)  :

The pushout under the initial object is the coproduct

Equations
• H₁ H₂ =
def is_pushout_of_is_initial_is_coproduct {C : Type u} {W X Y Z : C} (f : X Z) (g : Y Z) (h : W X) (k : W Y)  :

The coproduct is the pushout under the initial object.

Equations
• H₁ H₂ = (λ (s : , , _⟩)

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

Equations

Any category with pushouts and initial object has binary coproducts.

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

Equations
noncomputable def coprod_iso_pushout {C : Type u} (X Y : C)  :

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

Equations