# mathlibdocumentation

category_theory.limits.preserves.shapes.products

# Preserving products #

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

In particular, we show that pi_comparison G f is an isomorphism iff G preserves the limit of f.

def category_theory.limits.is_limit_map_cone_fan_mk_equiv {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), P f j) :
category_theory.limits.is_limit (λ (j : J), G.map (g j)))

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

Equations
def category_theory.limits.is_limit_fan_mk_obj_of_is_limit {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), P f j)  :
category_theory.limits.is_limit (λ (j : J), G.map (g j)))

The property of preserving products expressed in terms of fans.

Equations
def category_theory.limits.is_limit_of_is_limit_fan_mk_obj {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), P f j) (t : category_theory.limits.is_limit (λ (j : J), G.map (g j)))) :

The property of reflecting products expressed in terms of fans.

Equations
noncomputable def category_theory.limits.is_limit_of_has_product_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C)  :

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

Equations
noncomputable def category_theory.limits.preserves_product.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :

If pi_comparison G f is an isomorphism, then G preserves the limit of f.

Equations
noncomputable def category_theory.limits.preserves_product.iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :
G.obj ( f) λ (j : J), G.obj (f j)

If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

Equations
@[simp]
theorem category_theory.limits.preserves_product.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :
@[protected, instance]
def category_theory.limits.pi_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :
def category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), f j P) :
category_theory.limits.is_colimit (λ (j : J), G.map (g j)))

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

Equations
def category_theory.limits.is_colimit_cofan_mk_obj_of_is_colimit {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), f j P)  :
category_theory.limits.is_colimit (λ (j : J), G.map (g j)))

The property of preserving coproducts expressed in terms of cofans.

Equations
def category_theory.limits.is_colimit_of_is_colimit_cofan_mk_obj {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) {P : C} (g : Π (j : J), f j P) (t : category_theory.limits.is_colimit (λ (j : J), G.map (g j)))) :

The property of reflecting coproducts expressed in terms of cofans.

Equations
noncomputable def category_theory.limits.is_colimit_of_has_coproduct_of_preserves_colimit {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C)  :

If G preserves coproducts and C has them, then the cofan constructed of the mapped inclusion of a coproduct is a colimit.

Equations
noncomputable def category_theory.limits.preserves_coproduct.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_coproduct (λ (j : J), G.obj (f j))]  :

If sigma_comparison G f is an isomorphism, then G preserves the colimit of f.

Equations
noncomputable def category_theory.limits.preserves_coproduct.iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_coproduct (λ (j : J), G.obj (f j))]  :
G.obj ( f) λ (j : J), G.obj (f j)

If G preserves colimits, we have an isomorphism from the image of a coproduct to the coproduct of the images.

Equations
@[simp]
theorem category_theory.limits.preserves_coproduct.inv_hom {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_coproduct (λ (j : J), G.obj (f j))]  :
@[protected, instance]
def category_theory.limits.sigma_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_coproduct (λ (j : J), G.obj (f j))]  :