# mathlibdocumentation

category_theory.limits.preserves.shapes

def preserves_products_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (f : J → C)  :
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 preserves_products_iso_hom_π {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (f : J → C) (j : J) :
.hom category_theory.limits.pi.π (λ (j : J), G.obj (f j)) j = G.map

@[simp]
theorem preserves_products_iso_hom_π_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (f : J → C) (j : J) {X' : D} (f' : G.obj (f j) X') :
.hom category_theory.limits.pi.π (λ (j : J), G.obj (f j)) j f' = G.map f'

@[simp]
theorem map_lift_comp_preserves_products_iso_hom {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.pi.lift (λ (j : J), G.map (g j))

@[simp]
theorem map_lift_comp_preserves_products_iso_hom_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type v} (f : J → C) (P : C) (g : Π (j : J), P f j) {X' : D} (f' : ( λ (j : J), G.obj (f j)) X') :
.hom f' = category_theory.limits.pi.lift (λ (j : J), G.map (g j)) f'