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.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] :
G.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (j : J) {Z : D} (h : G.toPrefunctor.obj (F.toPrefunctor.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.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (j : J) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F G) j) = G.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (j : J) {Z : D} (h : G.toPrefunctor.obj (F.toPrefunctor.obj j) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (j : J) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).inv (G.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (t : CategoryTheory.Limits.Cone F) {Z : D} (h : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F G) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F G)] (t : CategoryTheory.Limits.Cone F) :
    CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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
    @[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).toPrefunctor.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
      @[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.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] :
      G.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (j : J) {Z : D} (h : G.toPrefunctor.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.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (j : J) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F G) j) (CategoryTheory.preservesColimitIso G F).inv = G.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (j : J) {Z : D} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F G) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (j : J) :
        CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (t : CategoryTheory.Limits.Cocone F) {Z : D} (h : G.toPrefunctor.obj t.pt ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.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] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F G)] (t : CategoryTheory.Limits.Cocone F) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (G.toPrefunctor.map (CategoryTheory.Limits.colimit.desc F t)) = CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp F G) (G.mapCocone t)
        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).toPrefunctor.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