# 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_limit_pair.of_iso_prod_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_limit_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_limit_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)]  :
def category_theory.limits.is_colimit_map_cocone_binary_cofan_equiv {C : Type u₁} {D : Type u₂} (G : C D) {P X Y : C} (f : X P) (g : Y P) :

The map of a binary cofan is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute binary_cofan.mk with functor.map_cocone.

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

The property of preserving coproducts expressed in terms of binary cofans.

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

The property of reflecting coproducts expressed in terms of binary cofans.

Equations

If G preserves binary coproducts and C has them, then the binary cofan constructed of the mapped morphisms of the binary product cocone is a colimit.

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

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

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

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

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