Isomorphisms about functors which preserve (co)limits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
If G preserves limits, and C and D have limits, then for any diagram F : J ⥤ C we have a
canonical isomorphism preserves_limit_iso : G.obj (limit F) ≅ limit (F ⋙ G).
We also show that we can commute is_limit.lift of a preserved limit with functor.map_cone:
(preserves_limit.preserves t).lift (G.map_cone c₂) = G.map (t.lift c₂).
The duals of these are also given. For functors which preserve (co)limits of specific shapes, see
preserves/shapes.lean.
@[simp]
theorem
category_theory.preserves_lift_map_cone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
(c₁ c₂ : category_theory.limits.cone F)
(t : category_theory.limits.is_limit c₁) :
noncomputable
def
category_theory.preserves_limit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[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 limit of a functor F
to the limit of the functor F ⋙ G.
@[simp]
theorem
category_theory.preserves_limits_iso_hom_π
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J) :
(category_theory.preserves_limit_iso G F).hom ≫ category_theory.limits.limit.π (F ⋙ G) j = G.map (category_theory.limits.limit.π F j)
@[simp]
theorem
category_theory.preserves_limits_iso_hom_π_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J)
{X' : D}
(f' : (F ⋙ G).obj j ⟶ X') :
(category_theory.preserves_limit_iso G F).hom ≫ category_theory.limits.limit.π (F ⋙ G) j ≫ f' = G.map (category_theory.limits.limit.π F j) ≫ f'
@[simp]
theorem
category_theory.preserves_limits_iso_inv_π_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J)
{X' : D}
(f' : G.obj (F.obj j) ⟶ X') :
(category_theory.preserves_limit_iso G F).inv ≫ G.map (category_theory.limits.limit.π F j) ≫ f' = category_theory.limits.limit.π (F ⋙ G) j ≫ f'
@[simp]
theorem
category_theory.preserves_limits_iso_inv_π
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(j : J) :
(category_theory.preserves_limit_iso G F).inv ≫ G.map (category_theory.limits.limit.π F j) = category_theory.limits.limit.π (F ⋙ G) j
@[simp]
theorem
category_theory.lift_comp_preserves_limits_iso_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(t : category_theory.limits.cone F) :
G.map (category_theory.limits.limit.lift F t) ≫ (category_theory.preserves_limit_iso G F).hom = category_theory.limits.limit.lift (F ⋙ G) (G.map_cone t)
@[simp]
theorem
category_theory.lift_comp_preserves_limits_iso_hom_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_limit F G]
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (F ⋙ G)]
(t : category_theory.limits.cone F)
{X' : D}
(f' : category_theory.limits.limit (F ⋙ G) ⟶ X') :
G.map (category_theory.limits.limit.lift F t) ≫ (category_theory.preserves_limit_iso G F).hom ≫ f' = category_theory.limits.limit.lift (F ⋙ G) (G.map_cone t) ≫ f'
@[simp]
theorem
category_theory.preserves_limit_nat_iso_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_limits_of_shape J G]
[category_theory.limits.has_limits_of_shape J D]
[category_theory.limits.has_limits_of_shape J C]
(X : J ⥤ C) :
noncomputable
def
category_theory.preserves_limit_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_limits_of_shape J G]
[category_theory.limits.has_limits_of_shape J D]
[category_theory.limits.has_limits_of_shape J C] :
If C, D has all limits of shape J, and G preserves them, then preserves_limit_iso is
functorial wrt F.
Equations
@[simp]
theorem
category_theory.preserves_limit_nat_iso_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_limits_of_shape J G]
[category_theory.limits.has_limits_of_shape J D]
[category_theory.limits.has_limits_of_shape J C]
(X : J ⥤ C) :
@[simp]
theorem
category_theory.preserves_desc_map_cocone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
(c₁ c₂ : category_theory.limits.cocone F)
(t : category_theory.limits.is_colimit c₁) :
(category_theory.limits.preserves_colimit.preserves t).desc (G.map_cocone c₂) = G.map (t.desc c₂)
noncomputable
def
category_theory.preserves_colimit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)] :
If G preserves colimits, we have an isomorphism from the image of the colimit of a functor F
to the colimit of the functor F ⋙ G.
@[simp]
theorem
category_theory.ι_preserves_colimits_iso_inv_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J)
{X' : D}
(f' : G.obj (category_theory.limits.colimit F) ⟶ X') :
category_theory.limits.colimit.ι (F ⋙ G) j ≫ (category_theory.preserves_colimit_iso G F).inv ≫ f' = G.map (category_theory.limits.colimit.ι F j) ≫ f'
@[simp]
theorem
category_theory.ι_preserves_colimits_iso_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J) :
category_theory.limits.colimit.ι (F ⋙ G) j ≫ (category_theory.preserves_colimit_iso G F).inv = G.map (category_theory.limits.colimit.ι F j)
@[simp]
theorem
category_theory.ι_preserves_colimits_iso_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J) :
G.map (category_theory.limits.colimit.ι F j) ≫ (category_theory.preserves_colimit_iso G F).hom = category_theory.limits.colimit.ι (F ⋙ G) j
@[simp]
theorem
category_theory.ι_preserves_colimits_iso_hom_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J)
{X' : D}
(f' : category_theory.limits.colimit (F ⋙ G) ⟶ X') :
G.map (category_theory.limits.colimit.ι F j) ≫ (category_theory.preserves_colimit_iso G F).hom ≫ f' = category_theory.limits.colimit.ι (F ⋙ G) j ≫ f'
@[simp]
theorem
category_theory.preserves_colimits_iso_inv_comp_desc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(t : category_theory.limits.cocone F) :
(category_theory.preserves_colimit_iso G F).inv ≫ G.map (category_theory.limits.colimit.desc F t) = category_theory.limits.colimit.desc (F ⋙ G) (G.map_cocone t)
@[simp]
theorem
category_theory.preserves_colimits_iso_inv_comp_desc_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.preserves_colimit F G]
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (F ⋙ G)]
(t : category_theory.limits.cocone F)
{X' : D}
(f' : G.obj t.X ⟶ X') :
(category_theory.preserves_colimit_iso G F).inv ≫ G.map (category_theory.limits.colimit.desc F t) ≫ f' = category_theory.limits.colimit.desc (F ⋙ G) (G.map_cocone t) ≫ f'
noncomputable
def
category_theory.preserves_colimit_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_colimits_of_shape J G]
[category_theory.limits.has_colimits_of_shape J D]
[category_theory.limits.has_colimits_of_shape J C] :
If C, D has all colimits of shape J, and G preserves them, then preserves_colimit_iso
is functorial wrt F.
Equations
@[simp]
theorem
category_theory.preserves_colimit_nat_iso_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_colimits_of_shape J G]
[category_theory.limits.has_colimits_of_shape J D]
[category_theory.limits.has_colimits_of_shape J C]
(X : J ⥤ C) :
@[simp]
theorem
category_theory.preserves_colimit_nat_iso_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(G : C ⥤ D)
{J : Type w}
[category_theory.category J]
[category_theory.limits.preserves_colimits_of_shape J G]
[category_theory.limits.has_colimits_of_shape J D]
[category_theory.limits.has_colimits_of_shape J C]
(X : J ⥤ C) :