# mathlibdocumentation

category_theory.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 has_limit classes.

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

## Future work #

The dual statement.

structure category_theory.limits.diagram_of_cones {J K : Type v} {C : Type u} (F : J K C) :
Type (max u v)

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

Instances for category_theory.limits.diagram_of_cones
@[simp]
theorem category_theory.limits.diagram_of_cones.cone_points_map {J K : Type v} {C : Type u} {F : J K C} (j j' : J) (f : j j') :
D.cone_points.map f = (D.map f).hom
def category_theory.limits.diagram_of_cones.cone_points {J K : Type v} {C : Type u} {F : J K C}  :
J C

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

Equations
@[simp]
theorem category_theory.limits.diagram_of_cones.cone_points_obj {J K : Type v} {C : Type u} {F : J K C} (j : J) :
D.cone_points.obj j = (D.obj j).X
def category_theory.limits.cone_of_cone_uncurry {J K : Type v} {C : Type u} {F : J K C} (Q : Π (j : J), )  :

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
@[simp]
theorem category_theory.limits.cone_of_cone_uncurry_π_app {J K : Type v} {C : Type u} {F : J K C} (Q : Π (j : J), ) (j : J) :
= (Q j).lift {X := c.X, π := {app := λ (k : K), c.π.app (j, k), naturality' := _}}
@[simp]
theorem category_theory.limits.cone_of_cone_uncurry_X {J K : Type v} {C : Type u} {F : J K C} (Q : Π (j : J), )  :
def category_theory.limits.cone_of_cone_uncurry_is_limit {J K : Type v} {C : Type u} {F : J K C} (Q : Π (j : J), )  :

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

Equations
noncomputable def category_theory.limits.diagram_of_cones.mk_of_has_limits {J K : Type v} {C : Type u} (F : J K C)  :

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
@[simp]
theorem category_theory.limits.diagram_of_cones.mk_of_has_limits_obj {J K : Type v} {C : Type u} (F : J K C) (j : J) :
@[simp]
theorem category_theory.limits.diagram_of_cones.mk_of_has_limits_map_hom {J K : Type v} {C : Type u} (F : J K C) (j j' : J) (f : j j') :
@[protected, instance]
noncomputable def category_theory.limits.diagram_of_cones_inhabited {J K : Type v} {C : Type u} (F : J K C)  :
Equations
@[simp]
theorem category_theory.limits.diagram_of_cones.mk_of_has_limits_cone_points {J K : Type v} {C : Type u} (F : J K C)  :
noncomputable def category_theory.limits.limit_uncurry_iso_limit_comp_lim {J K : Type v} {C : Type u} (F : J K C)  :

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
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π {J K : Type v} {C : Type u} (F : J K C) {j : J} {k : K} :
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π_assoc {J K : Type v} {C : Type u} (F : J K C) {j : J} {k : K} {X' : C} (f' : (F.obj j).obj k X') :
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π {J K : Type v} {C : Type u} (F : J K C) {j : J} {k : K} :
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π_assoc {J K : Type v} {C : Type u} (F : J K C) {j : J} {k : K} {X' : C} (f' : (j, k) X') :
noncomputable def category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim {J K : Type v} {C : Type u} (F : J K C)  :

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

Equations
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_hom_π_π_assoc {J K : Type v} {C : Type u} (F : J K C) (j : J) (k : K) {X' : C} (f' : (F.obj j).obj k X') :
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_hom_π_π {J K : Type v} {C : Type u} (F : J K C) (j : J) (k : K) :
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_inv_π_π {J K : Type v} {C : Type u} (F : J K C) (k : K) (j : J) :
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_inv_π_π_assoc {J K : Type v} {C : Type u} (F : J K C) (k : K) (j : J) {X' : C} (f' : (F.flip.obj k).obj j X') :

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
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π_assoc {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} {X' : C} (f' : .obj j).obj k X') :
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} :
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π_assoc {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} {X' : C} (f' : G.obj (j, k) X') :
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} :
noncomputable def category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim {J K : Type v} {C : Type u} (G : J × K C)  :

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
@[simp]
theorem category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_hom_π_π {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} :
@[simp]
theorem category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_inv_π_π {J K : Type v} {C : Type u} (G : J × K C) {j : J} {k : K} :