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₁} [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₂)
source
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
    source
    @[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)
    source
    @[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
    source
    @[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_π.

    source
    @[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
    source
    @[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
    source
    @[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_π.

    source
    @[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)
    source
    @[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
    source
    @[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)

    Alias of CategoryTheory.lift_comp_preservesLimitIso_hom.

    source
    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)
    source
    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
    Instances For
      source
      @[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
      source
      @[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
      source
      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)] :
      Limits.PreservesLimit F G

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

      source
      @[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₂)
      source
      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
        source
        @[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)
        source
        @[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
        source
        @[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.

        source
        @[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
        source
        @[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
        source
        @[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.

        source
        @[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)
        source
        @[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
        source
        @[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)

        Alias of CategoryTheory.preservesColimitIso_inv_comp_desc.

        source
        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)
        source
        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
          source
          @[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
          source
          @[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
          source
          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)] :
          Limits.PreservesColimit F G

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