Isomorphisms about functors which preserve (co)limits #
If G preserves limits, and C and D have limits, then for any diagram F : J ⥤ C we have a
canonical isomorphism preservesLimitsIso : G.obj (Limit F) ≅ Limit (F ⋙ G).
We also show that we can commute IsLimit.lift of a preserved limit with Functor.mapCone:
(PreservesLimit.preserves t).lift (G.mapCone 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
CategoryTheory.preserves_lift_mapCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
(c₁ c₂ : Limits.Cone F)
(t : Limits.IsLimit c₁)
:
(Limits.isLimitOfPreserves G t).lift (G.mapCone c₂) = G.map (t.lift c₂)
def
CategoryTheory.preservesLimitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
:
G.obj (Limits.limit F) ≅ Limits.limit (F.comp 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.preservesLimitIso_hom_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
:
CategoryStruct.comp (preservesLimitIso G F).hom (Limits.limit.π (F.comp G) j) = G.map (Limits.limit.π F j)
@[simp]
theorem
CategoryTheory.preservesLimitIso_hom_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
{Z : D}
(h : G.obj (F.obj j) ⟶ Z)
:
CategoryStruct.comp (preservesLimitIso G F).hom (CategoryStruct.comp (Limits.limit.π (F.comp G) j) h) = CategoryStruct.comp (G.map (Limits.limit.π F j)) h
@[deprecated CategoryTheory.preservesLimitIso_hom_π (since := "2024-10-27")]
theorem
CategoryTheory.preservesLimitsIso_hom_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
:
CategoryStruct.comp (preservesLimitIso G F).hom (Limits.limit.π (F.comp G) j) = G.map (Limits.limit.π F j)
Alias of CategoryTheory.preservesLimitIso_hom_π.
@[simp]
theorem
CategoryTheory.preservesLimitIso_inv_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
:
CategoryStruct.comp (preservesLimitIso G F).inv (G.map (Limits.limit.π F j)) = Limits.limit.π (F.comp G) j
@[simp]
theorem
CategoryTheory.preservesLimitIso_inv_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
{Z : D}
(h : G.obj (F.obj j) ⟶ Z)
:
CategoryStruct.comp (preservesLimitIso G F).inv (CategoryStruct.comp (G.map (Limits.limit.π F j)) h) = CategoryStruct.comp (Limits.limit.π (F.comp G) j) h
@[deprecated CategoryTheory.preservesLimitIso_inv_π (since := "2024-10-27")]
theorem
CategoryTheory.preservesLimitsIso_inv_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(j : J)
:
CategoryStruct.comp (preservesLimitIso G F).inv (G.map (Limits.limit.π F j)) = Limits.limit.π (F.comp G) j
Alias of CategoryTheory.preservesLimitIso_inv_π.
@[simp]
theorem
CategoryTheory.lift_comp_preservesLimitIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(t : Limits.Cone F)
:
CategoryStruct.comp (G.map (Limits.limit.lift F t)) (preservesLimitIso G F).hom = Limits.limit.lift (F.comp G) (G.mapCone t)
@[simp]
theorem
CategoryTheory.lift_comp_preservesLimitIso_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(t : Limits.Cone F)
{Z : D}
(h : Limits.limit (F.comp G) ⟶ Z)
:
CategoryStruct.comp (G.map (Limits.limit.lift F t)) (CategoryStruct.comp (preservesLimitIso G F).hom h) = CategoryStruct.comp (Limits.limit.lift (F.comp G) (G.mapCone t)) h
@[deprecated CategoryTheory.lift_comp_preservesLimitIso_hom (since := "2024-10-27")]
theorem
CategoryTheory.lift_comp_preservesLimitsIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
(t : Limits.Cone F)
:
CategoryStruct.comp (G.map (Limits.limit.lift F t)) (preservesLimitIso G F).hom = Limits.limit.lift (F.comp G) (G.mapCone t)
instance
CategoryTheory.instIsIsoPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesLimit F G]
[Limits.HasLimit F]
:
IsIso (Limits.limit.post F G)
def
CategoryTheory.preservesLimitNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesLimitsOfShape J G]
[Limits.HasLimitsOfShape J D]
[Limits.HasLimitsOfShape J C]
:
Limits.lim.comp G ≅ ((whiskeringRight J C D).obj G).comp Limits.lim
If C, D has all limits of shape J, and G preserves them, then preservesLimitsIso is
functorial wrt F.
Equations
- CategoryTheory.preservesLimitNatIso G = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor J C) => CategoryTheory.preservesLimitIso G F) ⋯
Instances For
@[simp]
theorem
CategoryTheory.preservesLimitNatIso_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesLimitsOfShape J G]
[Limits.HasLimitsOfShape J D]
[Limits.HasLimitsOfShape J C]
(X : Functor J C)
:
(preservesLimitNatIso G).inv.app X = (preservesLimitIso G X).inv
@[simp]
theorem
CategoryTheory.preservesLimitNatIso_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesLimitsOfShape J G]
[Limits.HasLimitsOfShape J D]
[Limits.HasLimitsOfShape J C]
(X : Functor J C)
:
(preservesLimitNatIso G).hom.app X = (preservesLimitIso G X).hom
theorem
CategoryTheory.preservesLimit_of_isIso_post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.HasLimit F]
[Limits.HasLimit (F.comp G)]
[IsIso (Limits.limit.post F G)]
:
If the comparison morphism G.obj (limit F) ⟶ limit (F ⋙ G) is an isomorphism, then G
preserves limits of F.
@[simp]
theorem
CategoryTheory.preserves_desc_mapCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
(c₁ c₂ : Limits.Cocone F)
(t : Limits.IsColimit c₁)
:
(Limits.isColimitOfPreserves G t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
def
CategoryTheory.preservesColimitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
:
G.obj (Limits.colimit F) ≅ Limits.colimit (F.comp 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ι_preservesColimitIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
:
CategoryStruct.comp (Limits.colimit.ι (F.comp G) j) (preservesColimitIso G F).inv = G.map (Limits.colimit.ι F j)
@[simp]
theorem
CategoryTheory.ι_preservesColimitIso_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
{Z : D}
(h : G.obj (Limits.colimit F) ⟶ Z)
:
CategoryStruct.comp (Limits.colimit.ι (F.comp G) j) (CategoryStruct.comp (preservesColimitIso G F).inv h) = CategoryStruct.comp (G.map (Limits.colimit.ι F j)) h
@[deprecated CategoryTheory.ι_preservesColimitIso_inv (since := "2024-10-27")]
theorem
CategoryTheory.ι_preservesColimitsIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
:
CategoryStruct.comp (Limits.colimit.ι (F.comp G) j) (preservesColimitIso G F).inv = G.map (Limits.colimit.ι F j)
Alias of CategoryTheory.ι_preservesColimitIso_inv.
@[simp]
theorem
CategoryTheory.ι_preservesColimitIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
:
CategoryStruct.comp (G.map (Limits.colimit.ι F j)) (preservesColimitIso G F).hom = Limits.colimit.ι (F.comp G) j
@[simp]
theorem
CategoryTheory.ι_preservesColimitIso_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
{Z : D}
(h : Limits.colimit (F.comp G) ⟶ Z)
:
CategoryStruct.comp (G.map (Limits.colimit.ι F j)) (CategoryStruct.comp (preservesColimitIso G F).hom h) = CategoryStruct.comp (Limits.colimit.ι (F.comp G) j) h
@[deprecated CategoryTheory.ι_preservesColimitIso_hom (since := "2024-10-27")]
theorem
CategoryTheory.ι_preservesColimitsIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(j : J)
:
CategoryStruct.comp (G.map (Limits.colimit.ι F j)) (preservesColimitIso G F).hom = Limits.colimit.ι (F.comp G) j
Alias of CategoryTheory.ι_preservesColimitIso_hom.
@[simp]
theorem
CategoryTheory.preservesColimitIso_inv_comp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(t : Limits.Cocone F)
:
CategoryStruct.comp (preservesColimitIso G F).inv (G.map (Limits.colimit.desc F t)) = Limits.colimit.desc (F.comp G) (G.mapCocone t)
@[simp]
theorem
CategoryTheory.preservesColimitIso_inv_comp_desc_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(t : Limits.Cocone F)
{Z : D}
(h : G.obj t.pt ⟶ Z)
:
CategoryStruct.comp (preservesColimitIso G F).inv (CategoryStruct.comp (G.map (Limits.colimit.desc F t)) h) = CategoryStruct.comp (Limits.colimit.desc (F.comp G) (G.mapCocone t)) h
@[deprecated CategoryTheory.preservesColimitIso_inv_comp_desc (since := "2024-10-27")]
theorem
CategoryTheory.preservesColimitsIso_inv_comp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
(t : Limits.Cocone F)
:
CategoryStruct.comp (preservesColimitIso G F).inv (G.map (Limits.colimit.desc F t)) = Limits.colimit.desc (F.comp G) (G.mapCocone t)
instance
CategoryTheory.instIsIsoPost_1
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.PreservesColimit F G]
[Limits.HasColimit F]
:
IsIso (Limits.colimit.post F G)
def
CategoryTheory.preservesColimitNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesColimitsOfShape J G]
[Limits.HasColimitsOfShape J D]
[Limits.HasColimitsOfShape J C]
:
Limits.colim.comp G ≅ ((whiskeringRight J C D).obj G).comp Limits.colim
If C, D has all colimits of shape J, and G preserves them, then preservesColimitIso
is functorial wrt F.
Equations
Instances For
@[simp]
theorem
CategoryTheory.preservesColimitNatIso_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesColimitsOfShape J G]
[Limits.HasColimitsOfShape J D]
[Limits.HasColimitsOfShape J C]
(X : Functor J C)
:
(preservesColimitNatIso G).hom.app X = (preservesColimitIso G X).hom
@[simp]
theorem
CategoryTheory.preservesColimitNatIso_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
[Limits.PreservesColimitsOfShape J G]
[Limits.HasColimitsOfShape J D]
[Limits.HasColimitsOfShape J C]
(X : Functor J C)
:
(preservesColimitNatIso G).inv.app X = (preservesColimitIso G X).inv
theorem
CategoryTheory.preservesColimit_of_isIso_post
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
[Limits.HasColimit F]
[Limits.HasColimit (F.comp G)]
[IsIso (Limits.colimit.post F G)]
:
If the comparison morphism colimit (F ⋙ G) ⟶ G.obj (colimit F) is an isomorphism, then G
preserves colimits of F.