Documentation

Mathlib.CategoryTheory.Limits.Fubini

A Fubini theorem for categorical limits #

We prove that $lim_{J × K} G = lim_J (lim_K G(j, -))$ for a functor G : J × K ⥤ C, when all the appropriate limits exist.

We begin working with a functor F : J ⥤ K ⥤ C. We'll write G : J × K ⥤ C for the associated "uncurried" functor.

In the first part, given a coherent family D of limit cones over the functors F.obj j, and a cone c over G, we construct a cone over the cone points of D. We then show that if c is a limit cone, the constructed cone is also a limit cone.

In the second part, we state the Fubini theorem in the setting where limits are provided by suitable HasLimit classes.

We construct limitUncurryIsoLimitCompLim F : limit (uncurry.obj F) ≅ limit (F ⋙ lim) and give simp lemmas characterising it. For convenience, we also provide limitIsoLimitCurryCompLim G : limit G ≅ limit ((curry.obj G) ⋙ lim) in terms of the uncurried functor.

Future work #

The dual statement.

source
structure CategoryTheory.Limits.DiagramOfCones {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) :
Type (max u v)

A structure carrying a diagram of cones over the functors F.obj j.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.DiagramOfCones.conePoints_obj {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCones F) (j : J) :
    (CategoryTheory.Limits.DiagramOfCones.conePoints D).obj j = (CategoryTheory.Limits.DiagramOfCones.obj D j).pt
    source
    @[simp]
    theorem CategoryTheory.Limits.DiagramOfCones.conePoints_map {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCones F) :
    ∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.DiagramOfCones.conePoints D).map f = (CategoryTheory.Limits.DiagramOfCones.map D f).hom
    source
    def CategoryTheory.Limits.DiagramOfCones.conePoints {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCones F) :
    CategoryTheory.Functor J C

    Extract the functor J ⥤ C consisting of the cone points and the maps between them, from a DiagramOfCones.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.coneOfConeUncurry_π_app {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F} (Q : (j : J) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.DiagramOfCones.obj D j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) (j : J) :
      (CategoryTheory.Limits.coneOfConeUncurry Q c).π.app j = CategoryTheory.Limits.IsLimit.lift (Q j) { pt := c.pt, π := CategoryTheory.NatTrans.mk fun k => c.π.app (j, k) }
      source
      @[simp]
      theorem CategoryTheory.Limits.coneOfConeUncurry_pt {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F} (Q : (j : J) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.DiagramOfCones.obj D j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) :
      (CategoryTheory.Limits.coneOfConeUncurry Q c).pt = c.pt
      source
      def CategoryTheory.Limits.coneOfConeUncurry {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F} (Q : (j : J) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.DiagramOfCones.obj D j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) :
      CategoryTheory.Limits.Cone (CategoryTheory.Limits.DiagramOfCones.conePoints D)

      Given a diagram D of limit cones over the F.obj j, and a cone over uncurry.obj F, we can construct a cone over the diagram consisting of the cone points from D.

      Instances For
        source
        def CategoryTheory.Limits.coneOfConeUncurryIsLimit {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F} (Q : (j : J) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.DiagramOfCones.obj D j)) {c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)} (P : CategoryTheory.Limits.IsLimit c) :
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfConeUncurry Q c)

        coneOfConeUncurry Q c is a limit cone when c is a limit cone.

        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) :
          CategoryTheory.Limits.DiagramOfCones.obj (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F) j = CategoryTheory.Limits.limit.cone (F.obj j)
          source
          @[simp]
          theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] :
          ∀ {j j' : J} (f : j ⟶ j'), (CategoryTheory.Limits.DiagramOfCones.map (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F) f).hom = CategoryTheory.Limits.lim.map (F.map f)
          source
          noncomputable def CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] :
          CategoryTheory.Limits.DiagramOfCones F

          Given a functor F : J ⥤ K ⥤ C, with all needed limits, we can construct a diagram consisting of the limit cone over each functor F.obj j, and the universal cone morphisms between these.

          Instances For
            source
            noncomputable instance CategoryTheory.Limits.diagramOfConesInhabited {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] :
            Inhabited (CategoryTheory.Limits.DiagramOfCones F)
            source
            @[simp]
            theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] :
            CategoryTheory.Limits.DiagramOfCones.conePoints (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F) = CategoryTheory.Functor.comp F CategoryTheory.Limits.lim
            source
            noncomputable def CategoryTheory.Limits.limitUncurryIsoLimitCompLim {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] :
            CategoryTheory.Limits.limit (CategoryTheory.uncurry.obj F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)

            The Fubini theorem for a functor F : J ⥤ K ⥤ C, showing that the limit of uncurry.obj F can be computed as the limit of the limits of the functors F.obj j.

            Instances For
              source
              theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (F.obj j).obj k ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k)) h
              source
              @[simp]
              theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)) = CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k)
              source
              theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (CategoryTheory.uncurry.obj F).obj (j, k) ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
              source
              @[simp]
              theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv (CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.obj F) (j, k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)
              source
              noncomputable def CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape (J × K) C] [CategoryTheory.Limits.HasLimitsOfShape (K × J) C] :
              CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.lim) ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)

              The limit of F.flip ⋙ lim is isomorphic to the limit of F ⋙ lim.

              Instances For
                source
                theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape (J × K) C] [CategoryTheory.Limits.HasLimitsOfShape (K × J) C] (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.flip F).obj k) j) h)
                source
                @[simp]
                theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape (J × K) C] [CategoryTheory.Limits.HasLimitsOfShape (K × J) C] (j : J) (k : K) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.flip F).obj k) j)
                source
                theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape (J × K) C] [CategoryTheory.Limits.HasLimitsOfShape (K × J) C] (k : K) (j : J) {Z : C} (h : ((CategoryTheory.Functor.flip F).obj k).obj j ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.flip F).obj k) j) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
                source
                @[simp]
                theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimitsOfShape (J × K) C] [CategoryTheory.Limits.HasLimitsOfShape (K × J) C] (k : K) (j : J) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.flip F).obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.obj j) k)
                source
                noncomputable def CategoryTheory.Limits.limitIsoLimitCurryCompLim {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit G] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] :
                CategoryTheory.Limits.limit G ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)

                The Fubini theorem for a functor G : J × K ⥤ C, showing that the limit of G can be computed as the limit of the limits of the functors G.obj (j, _).

                Instances For
                  source
                  theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit G] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : ((CategoryTheory.curry.obj G).obj j).obj k ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h
                  source
                  @[simp]
                  theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit G] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) = CategoryTheory.Limits.limit.π G (j, k)
                  source
                  theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit G] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : G.obj (j, k) ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k) h)
                  source
                  @[simp]
                  theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape K C] [CategoryTheory.Limits.HasLimit G] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} :
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv (CategoryTheory.Limits.limit.π G (j, k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)
                  source
                  noncomputable def CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimits C] :
                  CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)

                  A variant of the Fubini theorem for a functor G : J × K ⥤ C, showing that $\lim_k \lim_j G(j,k) ≅ \lim_j \lim_k G(j,k)$.

                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimits C] {j : J} {k : K} :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).obj k) j)
                    source
                    @[simp]
                    theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {J : Type v} {K : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.SmallCategory K] {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimits C] {j : J} {k : K} :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)