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_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
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.

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_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
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.

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