# mathlibdocumentation

category_theory.limits.preserves.shapes.binary_products

# Preserving binary products #

Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.

In particular, we show that prod_comparison G X Y is an isomorphism iff G preserves the product of X and Y.

def category_theory.limits.is_limit_map_cone_binary_fan_equiv {C : Type u₁} {D : Type u₂} (G : C D) {P X Y : C} (f : P X) (g : P Y) :

The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute binary_fan.mk with functor.map_cone.

Equations
def category_theory.limits.map_is_limit_of_preserves_of_is_limit {C : Type u₁} {D : Type u₂} (G : C D) {P X Y : C} (f : P X) (g : P Y)  :

The property of preserving products expressed in terms of binary fans.

Equations
def category_theory.limits.is_limit_of_reflects_of_map_is_limit {C : Type u₁} {D : Type u₂} (G : C D) {P X Y : C} (f : P X) (g : P Y) (l : category_theory.limits.is_limit (G.map g))) :

The property of reflecting products expressed in terms of binary fans.

Equations

If G preserves binary products and C has them, then the binary fan constructed of the mapped morphisms of the binary product cone is a limit.

Equations
def category_theory.limits.preserves_pair.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) (X Y : C) [ (G.obj Y)]  :

If the product comparison map for G at (X,Y) is an isomorphism, then G preserves the pair of (X,Y).

Equations
def category_theory.limits.preserves_pair.iso {C : Type u₁} {D : Type u₂} (G : C D) (X Y : C) [ (G.obj Y)]  :
G.obj (X Y) G.obj X G.obj Y

If G preserves the product of (X,Y), then the product comparison map for G at (X,Y) is an isomorphism.

Equations
@[simp]
theorem category_theory.limits.preserves_pair.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) (X Y : C) [ (G.obj Y)]  :
@[instance]
def category_theory.limits.prod_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) (X Y : C) [ (G.obj Y)]  :
Equations