mathlib documentation


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} [category_theory.small_category J] [category_theory.small_category K] {C : Type u} [category_theory.category C] (F : J K C) :
Type (max u v)

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

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


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.


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.