# Documentation

Mathlib.CategoryTheory.Limits.Fubini

# A Fubini theorem for categorical limits #

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

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

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

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

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

## Future work #

The dual statement.

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
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.conePoints_obj {J : Type v} {K : Type v} {C : Type u} {F : } (j : J) :
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.conePoints_map {J : Type v} {K : Type v} {C : Type u} {F : } :
∀ {X Y : J} (f : X Y),
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.

Instances For
@[simp]
theorem CategoryTheory.Limits.coneOfConeUncurry_π_app {J : Type v} {K : Type v} {C : Type u} {F : } (Q : ) (c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)) (j : J) :
.app j = CategoryTheory.Limits.IsLimit.lift (Q j) { pt := c.pt, π := CategoryTheory.NatTrans.mk fun k => c.app (j, k) }
@[simp]
theorem CategoryTheory.Limits.coneOfConeUncurry_pt {J : Type v} {K : Type v} {C : Type u} {F : } (Q : ) (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 : ) (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.

Instances For
def CategoryTheory.Limits.coneOfConeUncurryIsLimit {J : Type v} {K : Type v} {C : Type u} {F : } (Q : ) {c : CategoryTheory.Limits.Cone (CategoryTheory.uncurry.obj F)} :

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

Instances For
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj {J : Type v} {K : Type v} {C : Type u} (F : ) (j : J) :
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom {J : Type v} {K : Type v} {C : Type u} (F : ) :
∀ {j j' : J} (f : j j'), = CategoryTheory.Limits.lim.map (F.map f)
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.

Instances For
noncomputable instance CategoryTheory.Limits.diagramOfConesInhabited {J : Type v} {K : Type v} {C : Type u} (F : ) :
@[simp]
theorem CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints {J : Type v} {K : Type v} {C : Type u} (F : ) :
= CategoryTheory.Functor.comp F 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 (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] :
CategoryTheory.Limits.limit (CategoryTheory.uncurry.obj F) CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)

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

Instances For
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 (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (F.obj j).obj k Z) :
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 (CategoryTheory.Functor.comp F CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : (CategoryTheory.uncurry.obj F).obj (j, k) Z) :
noncomputable def CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim {J : Type v} {K : Type v} {C : Type u} (F : ) [] [] :

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

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

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

Instances For
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.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : ((CategoryTheory.curry.obj G).obj j).obj k Z) :
@[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.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)) =
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.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} {Z : C} (h : G.obj (j, k) Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k) h)
@[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.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)] {j : J} {k : K} :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim) j) (CategoryTheory.Limits.limit.π ((CategoryTheory.curry.obj G).obj j) k)
noncomputable def CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim {J : Type v} {K : Type v} {C : Type u} (G : CategoryTheory.Functor (J × K) C) :
CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj ()) CategoryTheory.Limits.lim) CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.curry.obj G) CategoryTheory.Limits.lim)

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

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