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 u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_6)

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

• obj (j : J) : Cone (F.obj j)

  For each object, a cone.

• map {j j' : J} (f : j ⟶ j') : (Cones.postcompose (F.map f)).obj (self.obj j) ⟶ self.obj j'

  For each map, a map of cones.

• id (j : J) : (self.map (CategoryStruct.id j)).hom = CategoryStruct.id ((Cones.postcompose (F.map (CategoryStruct.id j))).obj (self.obj j)).pt
• comp {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃) : (self.map (CategoryStruct.comp f g)).hom = CategoryStruct.comp (self.map f).hom (self.map g).hom

structure CategoryTheory.Limits.DiagramOfCocones {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_6)

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

• obj (j : J) : Cocone (F.obj j)

  For each object, a cocone.

• map {j j' : J} (f : j ⟶ j') : self.obj j ⟶ (Cocones.precompose (F.map f)).obj (self.obj j')

  For each map, a map of cocones.

• id (j : J) : (self.map (CategoryStruct.id j)).hom = CategoryStruct.id (self.obj j).pt
• comp {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃) : (self.map (CategoryStruct.comp f g)).hom = CategoryStruct.comp (self.map f).hom (self.map g).hom

def CategoryTheory.Limits.DiagramOfCones.conePoints {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCones F) : Functor J C

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 := ⋯ }

@[simp]

theorem CategoryTheory.Limits.DiagramOfCones.conePoints_obj {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCones F) (j : J) : D.conePoints.obj j = (D.obj j).pt

@[simp]

theorem CategoryTheory.Limits.DiagramOfCones.conePoints_map {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCones F) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : D.conePoints.map f = (D.map f).hom

def CategoryTheory.Limits.DiagramOfCocones.coconePoints {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCocones F) : Functor J C

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 := ⋯ }

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_obj {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCocones F) (j : J) : D.coconePoints.obj j = (D.obj j).pt

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_map {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} (D : DiagramOfCocones F) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : D.coconePoints.map f = (D.map f).hom

def CategoryTheory.Limits.coneOfConeUncurry {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCones F} (Q : (j : J) → IsLimit (D.obj j)) (c : Cone (uncurry.obj F)) : Cone D.conePoints

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.

@[simp]

theorem CategoryTheory.Limits.coneOfConeUncurry_pt {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCones F} (Q : (j : J) → IsLimit (D.obj j)) (c : Cone (uncurry.obj F)) : (coneOfConeUncurry Q c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.coneOfConeUncurry_π_app {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCones F} (Q : (j : J) → IsLimit (D.obj j)) (c : Cone (uncurry.obj F)) (j : J) : (coneOfConeUncurry Q c).π.app j = (Q j).lift { pt := c.pt, π := { app := fun (k : K) => c.π.app (j, k), naturality := ⋯ } }

def CategoryTheory.Limits.coconeOfCoconeUncurry {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCocones F} (Q : (j : J) → IsColimit (D.obj j)) (c : Cocone (uncurry.obj F)) : Cocone D.coconePoints

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.

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeUncurry_pt {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCocones F} (Q : (j : J) → IsColimit (D.obj j)) (c : Cocone (uncurry.obj F)) : (coconeOfCoconeUncurry Q c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCocones F} (Q : (j : J) → IsColimit (D.obj j)) (c : Cocone (uncurry.obj F)) (j : J) : (coconeOfCoconeUncurry Q c).ι.app j = (Q j).desc { pt := c.pt, ι := { app := fun (k : K) => c.ι.app (j, k), naturality := ⋯ } }

def CategoryTheory.Limits.coneOfConeUncurryIsLimit {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCones F} (Q : (j : J) → IsLimit (D.obj j)) {c : Cone (uncurry.obj F)} (P : IsLimit c) : IsLimit (coneOfConeUncurry Q c)

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.

def CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] {F : Functor J (Functor K C)} {D : DiagramOfCocones F} (Q : (j : J) → IsColimit (D.obj j)) {c : Cocone (uncurry.obj F)} (P : IsColimit c) : IsColimit (coconeOfCoconeUncurry Q c)

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.

noncomputable def CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] : 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.

Equations

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

@[simp]

theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] {j✝ j'✝ : J} (f : j✝ ⟶ j'✝) : ((mkOfHasLimits F).map f).hom = lim.map (F.map f)

@[simp]

theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] (j : J) : (mkOfHasLimits F).obj j = limit.cone (F.obj j)

noncomputable instance CategoryTheory.Limits.diagramOfConesInhabited {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] : Inhabited (DiagramOfCones F)

Equations

• CategoryTheory.Limits.diagramOfConesInhabited F = { default := CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F }

@[simp]

theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_5, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] : (mkOfHasLimits F).conePoints = F.comp lim

noncomputable def CategoryTheory.Limits.limitUncurryIsoLimitCompLim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] [HasLimit (uncurry.obj F)] [HasLimit (F.comp lim)] : limit (uncurry.obj F) ≅ limit (F.comp 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.

@[simp]

theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] [HasLimit (uncurry.obj F)] [HasLimit (F.comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitUncurryIsoLimitCompLim F).hom (CategoryStruct.comp (limit.π (F.comp lim) j) (limit.π (F.obj j) k)) = limit.π (uncurry.obj F) (j, k)

theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] [HasLimit (uncurry.obj F)] [HasLimit (F.comp lim)] {j : J} {k : K} {Z : C} (h : (F.obj j).obj k ⟶ Z) : CategoryStruct.comp (limitUncurryIsoLimitCompLim F).hom (CategoryStruct.comp (limit.π (F.comp lim) j) (CategoryStruct.comp (limit.π (F.obj j) k) h)) = CategoryStruct.comp (limit.π (uncurry.obj F) (j, k)) h

@[simp]

theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] [HasLimit (uncurry.obj F)] [HasLimit (F.comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitUncurryIsoLimitCompLim F).inv (limit.π (uncurry.obj F) (j, k)) = CategoryStruct.comp (limit.π (F.comp lim) j) (limit.π (F.obj j) k)

theorem CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape K C] [HasLimit (uncurry.obj F)] [HasLimit (F.comp lim)] {j : J} {k : K} {Z : C} (h : (uncurry.obj F).obj (j, k) ⟶ Z) : CategoryStruct.comp (limitUncurryIsoLimitCompLim F).inv (CategoryStruct.comp (limit.π (uncurry.obj F) (j, k)) h) = CategoryStruct.comp (limit.π (F.comp lim) j) (CategoryStruct.comp (limit.π (F.obj j) k) h)

noncomputable def CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] : DiagramOfCocones 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.

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_obj {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] (j : J) : (mkOfHasColimits F).obj j = colimit.cocone (F.obj j)

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] {j✝ j'✝ : J} (f : j✝ ⟶ j'✝) : ((mkOfHasColimits F).map f).hom = colim.map (F.map f)

noncomputable instance CategoryTheory.Limits.diagramOfCoconesInhabited {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] : Inhabited (DiagramOfCocones F)

Equations

• CategoryTheory.Limits.diagramOfCoconesInhabited F = { default := CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F }

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_coconePoints {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_5, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] : (mkOfHasColimits F).coconePoints = F.comp colim

noncomputable def CategoryTheory.Limits.colimitUncurryIsoColimitCompColim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] [HasColimit (uncurry.obj F)] [HasColimit (F.comp colim)] : colimit (uncurry.obj F) ≅ colimit (F.comp 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.

@[simp]

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] [HasColimit (uncurry.obj F)] [HasColimit (F.comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) (colimitUncurryIsoColimitCompColim F).inv) = colimit.ι (uncurry.obj F) (j, k)

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] [HasColimit (uncurry.obj F)] [HasColimit (F.comp colim)] {j : J} {k : K} {Z : C} (h : colimit (uncurry.obj F) ⟶ Z) : CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) (CategoryStruct.comp (colimitUncurryIsoColimitCompColim F).inv h)) = CategoryStruct.comp (colimit.ι (uncurry.obj F) (j, k)) h

@[simp]

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] [HasColimit (uncurry.obj F)] [HasColimit (F.comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι (uncurry.obj F) (j, k)) (colimitUncurryIsoColimitCompColim F).hom = CategoryStruct.comp (colimit.ι (F.obj j) k) (colimit.ι (F.comp colim) j)

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape K C] [HasColimit (uncurry.obj F)] [HasColimit (F.comp colim)] {j : J} {k : K} {Z : C} (h : colimit (F.comp colim) ⟶ Z) : CategoryStruct.comp (colimit.ι (uncurry.obj F) (j, k)) (CategoryStruct.comp (colimitUncurryIsoColimitCompColim F).hom h) = CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) h)

noncomputable def CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape J C] [HasLimitsOfShape K C] [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] : limit (F.flip.comp lim) ≅ limit (F.comp 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.

@[simp]

theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape J C] [HasLimitsOfShape K C] [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] (j : J) (k : K) : CategoryStruct.comp (limitFlipCompLimIsoLimitCompLim F).hom (CategoryStruct.comp (limit.π (F.comp lim) j) (limit.π (F.obj j) k)) = CategoryStruct.comp (limit.π (F.flip.comp lim) k) (limit.π (F.flip.obj k) j)

theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape J C] [HasLimitsOfShape K C] [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z) : CategoryStruct.comp (limitFlipCompLimIsoLimitCompLim F).hom (CategoryStruct.comp (limit.π (F.comp lim) j) (CategoryStruct.comp (limit.π (F.obj j) k) h)) = CategoryStruct.comp (limit.π (F.flip.comp lim) k) (CategoryStruct.comp (limit.π (F.flip.obj k) j) h)

@[simp]

theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape J C] [HasLimitsOfShape K C] [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] (k : K) (j : J) : CategoryStruct.comp (limitFlipCompLimIsoLimitCompLim F).inv (CategoryStruct.comp (limit.π (F.flip.comp lim) k) (limit.π (F.flip.obj k) j)) = CategoryStruct.comp (limit.π (F.comp lim) j) (limit.π (F.obj j) k)

theorem CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasLimitsOfShape J C] [HasLimitsOfShape K C] [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] (k : K) (j : J) {Z : C} (h : (F.flip.obj k).obj j ⟶ Z) : CategoryStruct.comp (limitFlipCompLimIsoLimitCompLim F).inv (CategoryStruct.comp (limit.π (F.flip.comp lim) k) (CategoryStruct.comp (limit.π (F.flip.obj k) j) h)) = CategoryStruct.comp (limit.π (F.comp lim) j) (CategoryStruct.comp (limit.π (F.obj j) k) h)

noncomputable def CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape J C] [HasColimitsOfShape K C] [HasColimitsOfShape (J × K) C] [HasColimitsOfShape (K × J) C] : colimit (F.flip.comp colim) ≅ colimit (F.comp 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.

@[simp]

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape J C] [HasColimitsOfShape K C] [HasColimitsOfShape (J × K) C] [HasColimitsOfShape (K × J) C] (j : J) (k : K) : CategoryStruct.comp (colimit.ι (F.flip.obj k) j) (CategoryStruct.comp (colimit.ι (F.flip.comp colim) k) (colimitFlipCompColimIsoColimitCompColim F).hom) = CategoryStruct.comp (colimit.ι (F.obj j) k) (colimit.ι (F.comp colim) j)

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape J C] [HasColimitsOfShape K C] [HasColimitsOfShape (J × K) C] [HasColimitsOfShape (K × J) C] (j : J) (k : K) {Z : C} (h : colimit (F.comp colim) ⟶ Z) : CategoryStruct.comp (colimit.ι (F.flip.obj k) j) (CategoryStruct.comp (colimit.ι (F.flip.comp colim) k) (CategoryStruct.comp (colimitFlipCompColimIsoColimitCompColim F).hom h)) = CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) h)

@[simp]

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape J C] [HasColimitsOfShape K C] [HasColimitsOfShape (J × K) C] [HasColimitsOfShape (K × J) C] (k : K) (j : J) : CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) (colimitFlipCompColimIsoColimitCompColim F).inv) = CategoryStruct.comp (colimit.ι (F.flip.obj k) j) (colimit.ι (F.flip.comp colim) k)

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor J (Functor K C)) [HasColimitsOfShape J C] [HasColimitsOfShape K C] [HasColimitsOfShape (J × K) C] [HasColimitsOfShape (K × J) C] (k : K) (j : J) {Z : C} (h : colimit (F.flip.comp colim) ⟶ Z) : CategoryStruct.comp (colimit.ι (F.obj j) k) (CategoryStruct.comp (colimit.ι (F.comp colim) j) (CategoryStruct.comp (colimitFlipCompColimIsoColimitCompColim F).inv h)) = CategoryStruct.comp (colimit.ι (F.flip.obj k) j) (CategoryStruct.comp (colimit.ι (F.flip.comp colim) k) h)

noncomputable def CategoryTheory.Limits.limitIsoLimitCurryCompLim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] : limit G ≅ limit ((curry.obj G).comp 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.

@[simp]

theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitIsoLimitCurryCompLim G).hom (CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (limit.π ((curry.obj G).obj j) k)) = limit.π G (j, k)

theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} {Z : C} (h : ((curry.obj G).obj j).obj k ⟶ Z) : CategoryStruct.comp (limitIsoLimitCurryCompLim G).hom (CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (CategoryStruct.comp (limit.π ((curry.obj G).obj j) k) h)) = CategoryStruct.comp (limit.π G (j, k)) h

@[simp]

theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitIsoLimitCurryCompLim G).inv (limit.π G (j, k)) = CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (limit.π ((curry.obj G).obj j) k)

theorem CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} {Z : C} (h : G.obj (j, k) ⟶ Z) : CategoryStruct.comp (limitIsoLimitCurryCompLim G).inv (CategoryStruct.comp (limit.π G (j, k)) h) = CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (CategoryStruct.comp (limit.π ((curry.obj G).obj j) k) h)

noncomputable def CategoryTheory.Limits.colimitIsoColimitCurryCompColim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] : colimit G ≅ colimit ((curry.obj G).comp 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.

@[simp]

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (CategoryStruct.comp (colimit.ι ((curry.obj G).comp colim) j) (colimitIsoColimitCurryCompColim G).inv) = colimit.ι G (j, k)

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv_assoc {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} {Z : C} (h : colimit G ⟶ Z) : CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (CategoryStruct.comp (colimit.ι ((curry.obj G).comp colim) j) (CategoryStruct.comp (colimitIsoColimitCurryCompColim G).inv h)) = CategoryStruct.comp (colimit.ι G (j, k)) h

@[simp]

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι G (j, k)) (colimitIsoColimitCurryCompColim G).hom = CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (colimit.ι ((curry.obj G).comp colim) j)

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom_assoc {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} {Z : C} (h : colimit ((curry.obj G).comp colim) ⟶ Z) : CategoryStruct.comp (colimit.ι G (j, k)) (CategoryStruct.comp (colimitIsoColimitCurryCompColim G).hom h) = CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (CategoryStruct.comp (colimit.ι ((curry.obj G).comp colim) j) h)

noncomputable def CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimitsOfShape J C] [HasLimitsOfShape (K × J) C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] : limit ((curry.obj ((Prod.swap K J).comp G)).comp lim) ≅ limit ((curry.obj G).comp 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.

@[simp]

theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimitsOfShape J C] [HasLimitsOfShape (K × J) C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitCurrySwapCompLimIsoLimitCurryCompLim G).hom (CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (limit.π ((curry.obj G).obj j) k)) = CategoryStruct.comp (limit.π ((curry.obj ((Prod.swap K J).comp G)).comp lim) k) (limit.π ((curry.obj ((Prod.swap K J).comp G)).obj k) j)

@[simp]

theorem CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasLimitsOfShape K C] [HasLimitsOfShape J C] [HasLimitsOfShape (K × J) C] [HasLimit G] [HasLimit ((curry.obj G).comp lim)] {j : J} {k : K} : CategoryStruct.comp (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv (CategoryStruct.comp (limit.π ((curry.obj ((Prod.swap K J).comp G)).comp lim) k) (limit.π ((curry.obj ((Prod.swap K J).comp G)).obj k) j)) = CategoryStruct.comp (limit.π ((curry.obj G).comp lim) j) (limit.π ((curry.obj G).obj j) k)

noncomputable def CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim {J : Type u_1} {K : Type u_2} [Category.{u_4, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_6, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimitsOfShape J C] [HasColimitsOfShape (K × J) C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] : colimit ((curry.obj ((Prod.swap K J).comp G)).comp colim) ≅ colimit ((curry.obj G).comp 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.

@[simp]

theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {J : Type u_1} {K : Type u_2} [Category.{u_5, u_1} J] [Category.{u_6, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimitsOfShape J C] [HasColimitsOfShape (K × J) C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι ((curry.obj ((Prod.swap K J).comp G)).obj k) j) (CategoryStruct.comp (colimit.ι ((curry.obj ((Prod.swap K J).comp G)).comp colim) k) (colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom) = CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (colimit.ι ((curry.obj G).comp colim) j)

@[simp]

theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv {J : Type u_1} {K : Type u_2} [Category.{u_6, u_1} J] [Category.{u_5, u_2} K] {C : Type u_3} [Category.{u_4, u_3} C] (G : Functor (J × K) C) [HasColimitsOfShape K C] [HasColimitsOfShape J C] [HasColimitsOfShape (K × J) C] [HasColimit G] [HasColimit ((curry.obj G).comp colim)] {j : J} {k : K} : CategoryStruct.comp (colimit.ι ((curry.obj G).obj j) k) (CategoryStruct.comp (colimit.ι ((curry.obj G).comp colim) j) (colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv) = CategoryStruct.comp (colimit.ι ((curry.obj ((Prod.swap K J).comp G)).obj k) j) (colimit.ι ((curry.obj ((Prod.swap K J).comp G)).comp colim) k)