mathlib documentation

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.

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.

Equations

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

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