# 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 v} (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 v} (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 v} (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
def category_theory.limits.is_limit_of_has_product_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (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
def category_theory.limits.preserves_product.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (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
def category_theory.limits.preserves_product.iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (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 v} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :

@[instance]
def category_theory.limits.pi_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (f : J → C) [category_theory.limits.has_product (λ (j : J), G.obj (f j))]  :

Equations