mathlib documentation

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.

source
def category_theory.limits.is_limit_map_cone_binary_fan_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) :
category_theory.limits.is_limit (G.map_cone (category_theory.limits.binary_fan.mk f g)) ≃ category_theory.limits.is_limit (category_theory.limits.binary_fan.mk (G.map f) (G.map g))

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
source
def category_theory.limits.map_is_limit_of_preserves_of_is_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) [category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G] (l : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk f g)) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk (G.map f) (G.map g))

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

Equations
source
def category_theory.limits.is_limit_of_reflects_of_map_is_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) [category_theory.limits.reflects_limit (category_theory.limits.pair X Y) G] (l : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk (G.map f) (G.map g))) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk f g)

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

Equations
source
noncomputable def category_theory.limits.is_limit_of_has_binary_product_of_preserves_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_product X Y] [category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G] :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk (G.map category_theory.limits.prod.fst) (G.map category_theory.limits.prod.snd))

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
source
noncomputable def category_theory.limits.preserves_limit_pair.of_iso_prod_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (G.obj X) (G.obj Y)] [i : category_theory.is_iso (category_theory.limits.prod_comparison G X Y)] :
category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G

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

Equations
source
noncomputable def category_theory.limits.preserves_limit_pair.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (G.obj X) (G.obj Y)] [category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G] :
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
source
@[simp]
theorem category_theory.limits.preserves_limit_pair.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (G.obj X) (G.obj Y)] [category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G] :
(category_theory.limits.preserves_limit_pair.iso G X Y).hom = category_theory.limits.prod_comparison G X Y
source
@[protected, instance]
def category_theory.limits.prod_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (G.obj X) (G.obj Y)] [category_theory.limits.preserves_limit (category_theory.limits.pair X Y) G] :
category_theory.is_iso (category_theory.limits.prod_comparison G X Y)
source
def category_theory.limits.is_colimit_map_cocone_binary_cofan_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) :
category_theory.limits.is_colimit (G.map_cocone (category_theory.limits.binary_cofan.mk f g)) ≃ category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (G.map f) (G.map g))

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
source
def category_theory.limits.map_is_colimit_of_preserves_of_is_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) [category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G] (l : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk f g)) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (G.map f) (G.map g))

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

Equations
source
def category_theory.limits.is_colimit_of_reflects_of_map_is_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) [category_theory.limits.reflects_colimit (category_theory.limits.pair X Y) G] (l : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (G.map f) (G.map g))) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk f g)

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

Equations
source
noncomputable def category_theory.limits.is_colimit_of_has_binary_coproduct_of_preserves_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G] :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (G.map category_theory.limits.coprod.inl) (G.map category_theory.limits.coprod.inr))

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
source
noncomputable def category_theory.limits.preserves_colimit_pair.of_iso_coprod_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (G.obj X) (G.obj Y)] [i : category_theory.is_iso (category_theory.limits.coprod_comparison G X Y)] :
category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G

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

Equations
source
noncomputable def category_theory.limits.preserves_colimit_pair.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (G.obj X) (G.obj Y)] [category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G] :
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
source
@[simp]
theorem category_theory.limits.preserves_colimit_pair.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (G.obj X) (G.obj Y)] [category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G] :
(category_theory.limits.preserves_colimit_pair.iso G X Y).hom = category_theory.limits.coprod_comparison G X Y
source
@[protected, instance]
def category_theory.limits.coprod_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X Y : C) [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (G.obj X) (G.obj Y)] [category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) G] :
category_theory.is_iso (category_theory.limits.coprod_comparison G X Y)