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} [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.

• obj : (j : J) → CategoryTheory.Limits.Cone (F.toPrefunctor.obj j)

  For each object, a cone.

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

  For each map, a map of cones.

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

structure CategoryTheory.Limits.DiagramOfCocones {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 cocones over the functors F.obj j.

• obj : (j : J) → CategoryTheory.Limits.Cocone (F.toPrefunctor.obj j)

  For each object, a cocone.

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

  For each map, a map of cocones.

• id : ∀ (j : J), (self.map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (self.obj j).pt
• comp : ∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), (self.map (CategoryTheory.CategoryStruct.comp f g)).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} [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).toPrefunctor.map f = (D.map f).hom

@[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).toPrefunctor.obj j = (D.obj j).pt

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.

Equations

• CategoryTheory.Limits.DiagramOfCones.conePoints D = CategoryTheory.Functor.mk { obj := fun (j : J) => (D.obj j).pt, map := fun {X Y : J} (f : X ⟶ Y) => (D.map f).hom }

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_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.DiagramOfCocones F) : ∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.DiagramOfCocones.coconePoints D).toPrefunctor.map f = (D.map f).hom

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.coconePoints_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.DiagramOfCocones F) (j : J) : (CategoryTheory.Limits.DiagramOfCocones.coconePoints D).toPrefunctor.obj j = (D.obj j).pt

def CategoryTheory.Limits.DiagramOfCocones.coconePoints {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.DiagramOfCocones F) : CategoryTheory.Functor J C

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

Equations

• CategoryTheory.Limits.DiagramOfCocones.coconePoints D = CategoryTheory.Functor.mk { obj := fun (j : J) => (D.obj j).pt, map := fun {X Y : J} (f : X ⟶ Y) => (D.map f).hom }

@[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 (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.toPrefunctor.obj F)) (j : J) : (CategoryTheory.Limits.coneOfConeUncurry Q c).π.app j = (Q j).lift { pt := c.pt, π := CategoryTheory.NatTrans.mk fun (k : K) => c.π.app (j, k) }

@[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 (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.toPrefunctor.obj F)) : (CategoryTheory.Limits.coneOfConeUncurry Q c).pt = c.pt

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 (D.obj j)) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.toPrefunctor.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.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeUncurry_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.DiagramOfCocones F} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.toPrefunctor.obj F)) : (CategoryTheory.Limits.coconeOfCoconeUncurry Q c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeUncurry_ι_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.DiagramOfCocones F} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.toPrefunctor.obj F)) (j : J) : (CategoryTheory.Limits.coconeOfCoconeUncurry Q c).ι.app j = (Q j).desc { pt := c.pt, ι := CategoryTheory.NatTrans.mk fun (k : K) => c.ι.app (j, k) }

def CategoryTheory.Limits.coconeOfCoconeUncurry {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.DiagramOfCocones F} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.toPrefunctor.obj F)) : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.DiagramOfCocones.coconePoints D)

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.

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 (D.obj j)) {c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.toPrefunctor.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.

Equations

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

def CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit {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.DiagramOfCocones F} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) {c : CategoryTheory.Limits.Cocone (CategoryTheory.uncurry.toPrefunctor.obj F)} (P : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.

@[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.mkOfHasLimits F).map f).hom = CategoryTheory.Limits.lim.toPrefunctor.map (F.toPrefunctor.map f)

@[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.mkOfHasLimits F).obj j = CategoryTheory.Limits.limit.cone (F.toPrefunctor.obj j)

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.

Equations

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

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)

Equations

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

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

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.toPrefunctor.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] : CategoryTheory.Limits.limit (CategoryTheory.uncurry.toPrefunctor.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.

Equations

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

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.toPrefunctor.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (F.toPrefunctor.obj j).toPrefunctor.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.toPrefunctor.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)) h

@[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.toPrefunctor.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.toPrefunctor.obj j) k)) = CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)

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.toPrefunctor.obj F)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (CategoryTheory.uncurry.toPrefunctor.obj F).toPrefunctor.obj (j, k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.uncurry.toPrefunctor.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.toPrefunctor.obj j) k) h)

@[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.toPrefunctor.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.toPrefunctor.obj F) (j, k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.toPrefunctor.obj j) k)

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_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.HasColimitsOfShape K C] (j : J) : (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).obj j = CategoryTheory.Limits.colimit.cocone (F.toPrefunctor.obj j)

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_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.HasColimitsOfShape K C] : ∀ {j j' : J} (f : j ⟶ j'), ((CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).map f).hom = CategoryTheory.Limits.colim.toPrefunctor.map (F.toPrefunctor.map f)

noncomputable def CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits {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.HasColimitsOfShape K C] : CategoryTheory.Limits.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.

noncomputable instance CategoryTheory.Limits.diagramOfCoconesInhabited {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.HasColimitsOfShape K C] : Inhabited (CategoryTheory.Limits.DiagramOfCocones F)

Equations

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

@[simp]

theorem CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_coconePoints {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.HasColimitsOfShape K C] : CategoryTheory.Limits.DiagramOfCocones.coconePoints (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F) = CategoryTheory.Functor.comp F CategoryTheory.Limits.colim

noncomputable def CategoryTheory.Limits.colimitUncurryIsoColimitCompColim {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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.toPrefunctor.obj F)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim)] : CategoryTheory.Limits.colimit (CategoryTheory.uncurry.toPrefunctor.obj F) ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F 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.

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.toPrefunctor.obj F)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.uncurry.toPrefunctor.obj F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)) h

@[simp]

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.toPrefunctor.obj F)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv) = CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.toPrefunctor.obj F)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) h)

@[simp]

theorem CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.uncurry.toPrefunctor.obj F)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.uncurry.toPrefunctor.obj F) (j, k)) (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j)

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.

Equations

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

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.toPrefunctor.obj j).toPrefunctor.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.toPrefunctor.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).toPrefunctor.obj k) j) h)

@[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.toPrefunctor.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).toPrefunctor.obj k) j)

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).toPrefunctor.obj k).toPrefunctor.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).toPrefunctor.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.toPrefunctor.obj j) k) h)

@[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).toPrefunctor.obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π (F.toPrefunctor.obj j) k)

noncomputable def CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim {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.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape (J × K) C] [CategoryTheory.Limits.HasColimitsOfShape (K × J) C] : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F 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.

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_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.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape (J × K) C] [CategoryTheory.Limits.HasColimitsOfShape (K × J) C] (j : J) (k : K) {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.flip F).toPrefunctor.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) h)

@[simp]

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_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.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape (J × K) C] [CategoryTheory.Limits.HasColimitsOfShape (K × J) C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.flip F).toPrefunctor.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) k) (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j)

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_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.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape (J × K) C] [CategoryTheory.Limits.HasColimitsOfShape (K × J) C] (k : K) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.flip F).toPrefunctor.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) k) h)

@[simp]

theorem CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_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.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape (J × K) C] [CategoryTheory.Limits.HasColimitsOfShape (K × J) C] (k : K) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.flip F).toPrefunctor.obj k) j) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.colim) k)

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.toPrefunctor.obj G) CategoryTheory.Limits.lim)] : CategoryTheory.Limits.limit G ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.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, _).

Equations

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

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.toPrefunctor.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j).toPrefunctor.obj k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (j, k)) h

@[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.toPrefunctor.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.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k)) = CategoryTheory.Limits.limit.π G (j, k)

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.toPrefunctor.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : G.toPrefunctor.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.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) h)

@[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.toPrefunctor.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.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k)

noncomputable def CategoryTheory.Limits.colimitIsoColimitCurryCompColim {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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit G] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim)] : CategoryTheory.Limits.colimit G ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) 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.

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit G] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) h

@[simp]

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit G] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv) = CategoryTheory.Limits.colimit.ι G (j, k)

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit G] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j) h)

@[simp]

theorem CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_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.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit G] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j)

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.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.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)$.

Equations

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

@[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.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).toPrefunctor.obj k) j)

@[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.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.lim) k) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).toPrefunctor.obj k) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k)

noncomputable def CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim {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.HasColimits C] : CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.colim) ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) 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.

@[simp]

theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_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.HasColimits C] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).toPrefunctor.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.colim) k) (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j)

@[simp]

theorem CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_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.HasColimits C] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj G).toPrefunctor.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj G) CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)).toPrefunctor.obj k) j) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) G)) CategoryTheory.Limits.colim) k)