# A Fubini theorem for categorical (co)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.

All statements have their counterpart for colimits.

structure CategoryTheory.Limits.DiagramOfCones {J : Type v} {K : Type v} {C : Type u} (F : ) :
Type (max u v)

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

Instances For
theorem CategoryTheory.Limits.DiagramOfCones.id {J : Type v} {K : Type v} {C : Type u} {F : } (self : ) (j : J) :
(self.map ).hom = CategoryTheory.CategoryStruct.id (.obj (self.obj j)).pt
theorem CategoryTheory.Limits.DiagramOfCones.comp {J : Type v} {K : Type v} {C : Type u} {F : } (self : ) {j₁ : J} {j₂ : J} {j₃ : J} (f : j₁ j₂) (g : j₂ j₃) :
(self.map ).hom = CategoryTheory.CategoryStruct.comp (self.map f).hom (self.map g).hom
structure CategoryTheory.Limits.DiagramOfCocones {J : Type v} {K : Type v} {C : Type u} (F : ) :
Type (max u v)

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

Instances For
theorem CategoryTheory.Limits.DiagramOfCocones.id {J : Type v} {K : Type v} {C : Type u} {F : } (self : ) (j : J) :
(self.map ).hom = CategoryTheory.CategoryStruct.id (self.obj j).pt
theorem CategoryTheory.Limits.DiagramOfCocones.comp {J : Type v} {K : Type v} {C : Type u} {F : } (self : ) {j₁ : J} {j₂ : J} {j₃ : J} (f : j₁ j₂) (g : j₂ j₃) :
(self.map ).hom = CategoryTheory.CategoryStruct.comp (self.map f).hom (self.map g).hom
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.conePoints_map {J : Type v} {K : Type v} {C : Type u} {F : } :
∀ {X Y : J} (f : X Y), D.conePoints.map f = (D.map f).hom
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.conePoints_obj {J : Type v} {K : Type v} {C : Type u} {F : } (j : J) :
D.conePoints.obj j = (D.obj j).pt
def CategoryTheory.Limits.DiagramOfCones.conePoints {J : Type v} {K : Type v} {C : Type u} {F : } :

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

Equations
• D.conePoints = { obj := fun (j : J) => (D.obj j).pt, map := fun {X Y : J} (f : X Y) => (D.map f).hom, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_map {J : Type v} {K : Type v} {C : Type u} {F : } :
∀ {X Y : J} (f : X Y), D.coconePoints.map f = (D.map f).hom
@[simp]
theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_obj {J : Type v} {K : Type v} {C : Type u} {F : } (j : J) :
D.coconePoints.obj j = (D.obj j).pt

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

Equations
• D.coconePoints = { obj := fun (j : J) => (D.obj j).pt, map := fun {X Y : J} (f : X Y) => (D.map f).hom, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.Limits.coneOfConeUncurry_π_app {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) (j : J) :
.app j = (Q j).lift { pt := c.pt, π := { app := fun (k : K) => c.app (j, k), naturality := } }
@[simp]
theorem CategoryTheory.Limits.coneOfConeUncurry_pt {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) :
= c.pt
def CategoryTheory.Limits.coneOfConeUncurry {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.coconeOfCoconeUncurry_pt {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)) :
= c.pt
@[simp]
theorem CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)) (j : J) :
.app j = (Q j).desc { pt := c.pt, ι := { app := fun (k : K) => c.app (j, k), naturality := } }
def CategoryTheory.Limits.coconeOfCoconeUncurry {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)) :

Given a diagram D of colimit cocones over the F.obj j, and a cocone over uncurry.obj F, we can construct a cocone over the diagram consisting of the cocone points from D.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.coneOfConeUncurryIsLimit {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) {c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)} :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit {J : Type v} {K : Type v} {C : Type u} {F : } (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) {c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.obj F)} :

coconeOfCoconeUncurry Q c is a colimit cocone when c is a colimit cocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom {J : Type v} {K : Type v} {C : Type u} (F : ) :
∀ {j j' : J} (f : j j'), .hom = CategoryTheory.Limits.lim.map (F.map f)
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj {J : Type v} {K : Type v} {C : Type u} (F : ) (j : J) :
noncomputable def CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits {J : Type v} {K : Type v} {C : Type u} (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance CategoryTheory.Limits.diagramOfConesInhabited {J : Type v} {K : Type v} {C : Type u} (F : ) :
Equations
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints {J : Type v} {K : Type v} {C : Type u} (F : ) :
.conePoints = F.comp CategoryTheory.Limits.lim
noncomputable def CategoryTheory.Limits.limitUncurryIsoLimitCompLim {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] :
CategoryTheory.Limits.limit (CategoryTheory.uncurry.obj F) CategoryTheory.Limits.limit (F.comp 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (F.obj j).obj k Z) :
@[simp]
theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} :
theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (CategoryTheory.uncurry.obj F).obj (j, k) Z) :
@[simp]
theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasLimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K} :
@[simp]
theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_obj {J : Type v} {K : Type v} {C : Type u} (F : ) (j : J) :
@[simp]
theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom {J : Type v} {K : Type v} {C : Type u} (F : ) :
∀ {j j' : J} (f : j j'), .hom = CategoryTheory.Limits.colim.map (F.map f)
noncomputable def CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits {J : Type v} {K : Type v} {C : Type u} (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance CategoryTheory.Limits.diagramOfCoconesInhabited {J : Type v} {K : Type v} {C : Type u} (F : ) :
Equations
@[simp]
theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_coconePoints {J : Type v} {K : Type v} {C : Type u} (F : ) :
.coconePoints = F.comp CategoryTheory.Limits.colim
noncomputable def CategoryTheory.Limits.colimitUncurryIsoColimitCompColim {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] :
CategoryTheory.Limits.colimit (CategoryTheory.uncurry.obj F) CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.uncurry.obj F) Z) :
@[simp]
theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} :
theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim) Z) :
@[simp]
theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom {J : Type v} {K : Type v} {C : Type u} (F : ) [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} :
noncomputable def CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim {J : Type v} {K : Type v} {C : Type u} (F : ) [] [] :
CategoryTheory.Limits.limit (F.flip.comp CategoryTheory.Limits.lim) CategoryTheory.Limits.limit (F.comp CategoryTheory.Limits.lim)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [] [] (j : J) (k : K) {Z : C} (h : (F.obj j).obj k Z) :
theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc {J : Type v} {K : Type v} {C : Type u} (F : ) [] [] (k : K) (j : J) {Z : C} (h : (F.flip.obj k).obj j Z) :
noncomputable def CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim {J : Type v} {K : Type v} {C : Type u} (F : ) [] [] :
CategoryTheory.Limits.colimit (F.flip.comp CategoryTheory.Limits.colim) CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)

The colimit of F.flip ⋙ colim is isomorphic to the colimit of F ⋙ colim.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.limitIsoLimitCurryCompLim {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] :
CategoryTheory.Limits.limit ((CategoryTheory.curry.obj G).comp 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, _).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : ((CategoryTheory.curry.obj G).obj j).obj k Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k) h)) =
@[simp]
theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) =
theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : G.obj (j, k) Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k) h)
@[simp]
theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim)] {j : J} {k : K} :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)
noncomputable def CategoryTheory.Limits.colimitIsoColimitCurryCompColim {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasColimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)] :
CategoryTheory.Limits.colimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv_assoc {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasColimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j) ) =
@[simp]
theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasColimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j) ) =
theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom_assoc {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasColimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j) h)
@[simp]
theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasColimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j)
noncomputable def CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) :
CategoryTheory.Limits.limit ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.lim) CategoryTheory.Limits.limit ((CategoryTheory.curry.obj G).comp 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)$.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp G)).obj k) j)
@[simp]
theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj (().comp G)).obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)
noncomputable def CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) :
CategoryTheory.Limits.colimit ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.colim) CategoryTheory.Limits.colimit ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp G)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.colim) k) ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j)
@[simp]
theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj G).comp CategoryTheory.Limits.colim) j) ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp G)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.obj (().comp G)).comp CategoryTheory.Limits.colim) k)