Documentation

Mathlib.CategoryTheory.Limits.Preserves.Limits

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.

source
@[simp]
theorem CategoryTheory.preserves_lift_mapCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) (t : CategoryTheory.Limits.IsLimit c₁) :
(CategoryTheory.Limits.PreservesLimit.preserves t).lift (G.mapCone c₂) = G.map (t.lift c₂)
source
def CategoryTheory.preservesLimitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] :
G.obj (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.preservesLimitsIso_hom_π_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F G) j) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.π F j)) h
    source
    @[simp]
    theorem CategoryTheory.preservesLimitsIso_hom_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (j : J) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F G) j) = G.map (CategoryTheory.Limits.limit.π F j)
    source
    @[simp]
    theorem CategoryTheory.preservesLimitsIso_inv_π_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.π F j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F G) j) h
    source
    @[simp]
    theorem CategoryTheory.preservesLimitsIso_inv_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (j : J) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv (G.map (CategoryTheory.Limits.limit.π F j)) = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F G) j
    source
    @[simp]
    theorem CategoryTheory.lift_comp_preservesLimitsIso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F) {Z : D} (h : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F G) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F G) (G.mapCone t)) h
    source
    @[simp]
    theorem CategoryTheory.lift_comp_preservesLimitsIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F) :
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F t)) (CategoryTheory.preservesLimitIso G F).hom = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F G) (G.mapCone t)
    source
    instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorLimitLimitCompInstHasLimitCompPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesLimit F G] [CategoryTheory.Limits.HasLimit F] :
    CategoryTheory.IsIso (CategoryTheory.Limits.limit.post F G)
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.preservesLimitNatIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) :
    (CategoryTheory.preservesLimitNatIso G).hom.app X = (CategoryTheory.preservesLimitIso G X).hom
    source
    @[simp]
    theorem CategoryTheory.preservesLimitNatIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] (X : CategoryTheory.Functor J C) :
    (CategoryTheory.preservesLimitNatIso G).inv.app X = (CategoryTheory.preservesLimitIso G X).inv
    source
    def CategoryTheory.preservesLimitNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesLimitsOfShape J G] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.Limits.HasLimitsOfShape J C] :
    CategoryTheory.Functor.comp CategoryTheory.Limits.lim G ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight J C D).obj G) CategoryTheory.Limits.lim

    If C, D has all limits of shape J, and G preserves them, then preservesLimitsIso is functorial wrt F.

    Equations
    Instances For
      source
      def CategoryTheory.preservesLimitOfIsIsoPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] [CategoryTheory.IsIso (CategoryTheory.Limits.limit.post F G)] :
      CategoryTheory.Limits.PreservesLimit F G

      If the comparison morphism G.obj (limit F) ⟶ limit (F ⋙ G) is an isomorphism, then G preserves limits of F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.preserves_desc_mapCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] (c₁ : CategoryTheory.Limits.Cocone F) (c₂ : CategoryTheory.Limits.Cocone F) (t : CategoryTheory.Limits.IsColimit c₁) :
        (CategoryTheory.Limits.PreservesColimit.preserves t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
        source
        def CategoryTheory.preservesColimitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] :
        G.obj (CategoryTheory.Limits.colimit F) ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp 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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ι_preservesColimitsIso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (j : J) {Z : D} (h : G.obj (CategoryTheory.Limits.colimit F) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F G) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) h
          source
          @[simp]
          theorem CategoryTheory.ι_preservesColimitsIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (j : J) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F G) j) (CategoryTheory.preservesColimitIso G F).inv = G.map (CategoryTheory.Limits.colimit.ι F j)
          source
          @[simp]
          theorem CategoryTheory.ι_preservesColimitsIso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (j : J) {Z : D} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F G) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F G) j) h
          source
          @[simp]
          theorem CategoryTheory.ι_preservesColimitsIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (j : J) :
          CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) (CategoryTheory.preservesColimitIso G F).hom = CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F G) j
          source
          @[simp]
          theorem CategoryTheory.preservesColimitsIso_inv_comp_desc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) {Z : D} (h : G.obj t.pt ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.desc F t)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp F G) (G.mapCocone t)) h
          source
          @[simp]
          theorem CategoryTheory.preservesColimitsIso_inv_comp_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (G.map (CategoryTheory.Limits.colimit.desc F t)) = CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp F G) (G.mapCocone t)
          source
          instance CategoryTheory.instIsIsoColimitCompInstHasColimitCompObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorColimitPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] :
          CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post F G)
          Equations
          • ⋯ = ⋯
          source
          @[simp]
          theorem CategoryTheory.preservesColimitNatIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) :
          (CategoryTheory.preservesColimitNatIso G).hom.app X = (CategoryTheory.preservesColimitIso G X).hom
          source
          @[simp]
          theorem CategoryTheory.preservesColimitNatIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) :
          (CategoryTheory.preservesColimitNatIso G).inv.app X = (CategoryTheory.preservesColimitIso G X).inv
          source
          def CategoryTheory.preservesColimitNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] :
          CategoryTheory.Functor.comp CategoryTheory.Limits.colim G ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight J C D).obj G) CategoryTheory.Limits.colim

          If C, D has all colimits of shape J, and G preserves them, then preservesColimitIso is functorial wrt F.

          Equations
          Instances For
            source
            def CategoryTheory.preservesColimitOfIsIsoPost {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] [CategoryTheory.IsIso (CategoryTheory.Limits.colimit.post F G)] :
            CategoryTheory.Limits.PreservesColimit F G

            If the comparison morphism colimit (F ⋙ G) ⟶ G.obj (colimit F) is an isomorphism, then G preserves colimits of F.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For