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.

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

Instances For

    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

      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

        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

          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

            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