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.
- obj : Π (j : J), category_theory.limits.cone (F.obj j)
- map : Π {j j' : J} (f : j ⟶ j'), (category_theory.limits.cones.postcompose (F.map f)).obj (self.obj j) ⟶ self.obj j'
- id : (∀ (j : J), (self.map (𝟙 j)).hom = 𝟙 ((category_theory.limits.cones.postcompose (F.map (𝟙 j))).obj (self.obj j)).X) . "obviously"
- comp : (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), (self.map (f ≫ g)).hom = (self.map f).hom ≫ (self.map g).hom) . "obviously"
A structure carrying a diagram of cones over the functors F.obj j
.
Instances for category_theory.limits.diagram_of_cones
- category_theory.limits.diagram_of_cones.has_sizeof_inst
- category_theory.limits.diagram_of_cones_inhabited
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
.
cone_of_cone_uncurry Q c
is a limit cone when c
is a limit cone.`
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
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
- category_theory.limits.limit_uncurry_iso_limit_comp_lim F = let c : category_theory.limits.cone (category_theory.uncurry.obj F) := category_theory.limits.limit.cone (category_theory.uncurry.obj F), P : category_theory.limits.is_limit c := category_theory.limits.limit.is_limit (category_theory.uncurry.obj F), G : category_theory.limits.diagram_of_cones F := category_theory.limits.diagram_of_cones.mk_of_has_limits F, Q : Π (j : J), category_theory.limits.is_limit (G.obj j) := λ (j : J), category_theory.limits.limit.is_limit (F.obj j) in (category_theory.limits.cone_of_cone_uncurry_is_limit Q P).cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (F ⋙ category_theory.limits.lim))
The limit of F.flip ⋙ lim
is isomorphic to the limit of F ⋙ lim
.
Equations
- category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim F = (category_theory.limits.limit_uncurry_iso_limit_comp_lim F.flip).symm ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.uncurry_obj_flip F) ≪≫ category_theory.limits.has_limit.iso_of_equivalence (category_theory.prod.braiding K J) (category_theory.nat_iso.of_components (λ (_x : K × J), category_theory.iso.refl (((category_theory.prod.braiding K J).functor ⋙ category_theory.uncurry.obj F).obj _x)) _) ≪≫ category_theory.limits.limit_uncurry_iso_limit_comp_lim F
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, _)
.
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
- category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim G = ((category_theory.limits.limit_iso_limit_curry_comp_lim (category_theory.prod.swap K J ⋙ G)).symm ≪≫ category_theory.limits.has_limit.iso_of_equivalence (category_theory.prod.braiding K J) (category_theory.iso.refl ((category_theory.prod.braiding K J).functor ⋙ G))) ≪≫ category_theory.limits.limit_iso_limit_curry_comp_lim G _