def
preserves_limits_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)] :
G.obj (category_theory.limits.limit F) ≅ category_theory.limits.limit (F ⋙ G)
If G preserves limits, we have an isomorphism from the image of the chosen limit of a functor F
to the chosen limit of the functor F ⋙ G.
@[simp]
theorem
preserves_limits_iso_hom_π
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J) :
(preserves_limits_iso G F).hom ≫ category_theory.limits.limit.π (F ⋙ G) j = G.map (category_theory.limits.limit.π F j)
@[simp]
theorem
preserves_limits_iso_hom_π_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J)
{X' : D}
(f' : (F ⋙ G).obj j ⟶ X') :
(preserves_limits_iso G F).hom ≫ category_theory.limits.limit.π (F ⋙ G) j ≫ f' = G.map (category_theory.limits.limit.π F j) ≫ f'
def
preserves_products_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
(f : J → C)
[category_theory.limits.has_limits C]
[category_theory.limits.has_limits D] :
If G preserves limits, we have an isomorphism
from the image of a product to the product of the images.
@[simp]
theorem
preserves_products_iso_hom_π_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
(f : J → C)
[category_theory.limits.has_limits C]
[category_theory.limits.has_limits D]
(j : J)
{X' : D}
(f' : G.obj (f j) ⟶ X') :
(preserves_products_iso G f).hom ≫ category_theory.limits.pi.π (λ (j : J), G.obj (f j)) j ≫ f' = G.map (category_theory.limits.pi.π f j) ≫ f'
@[simp]
theorem
preserves_products_iso_hom_π
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
(f : J → C)
[category_theory.limits.has_limits C]
[category_theory.limits.has_limits D]
(j : J) :
(preserves_products_iso G f).hom ≫ category_theory.limits.pi.π (λ (j : J), G.obj (f j)) j = G.map (category_theory.limits.pi.π f j)
@[simp]
theorem
map_lift_comp_preserves_products_iso_hom_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
(f : J → C)
[category_theory.limits.has_limits C]
[category_theory.limits.has_limits D]
(P : C)
(g : Π (j : J), P ⟶ f j)
{X' : D}
(f' : (∏ λ (j : J), G.obj (f j)) ⟶ X') :
G.map (category_theory.limits.pi.lift g) ≫ (preserves_products_iso G f).hom ≫ f' = category_theory.limits.pi.lift (λ (j : J), G.map (g j)) ≫ f'
@[simp]
theorem
map_lift_comp_preserves_products_iso_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.limits.preserves_limits G]
{J : Type v}
(f : J → C)
[category_theory.limits.has_limits C]
[category_theory.limits.has_limits D]
(P : C)
(g : Π (j : J), P ⟶ f j) :
G.map (category_theory.limits.pi.lift g) ≫ (preserves_products_iso G f).hom = category_theory.limits.pi.lift (λ (j : J), G.map (g j))