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 we have chosen limits
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.
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] :
- 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 (c.obj j) ⟶ c.obj j'
- id : (∀ (j : J), (c.map (𝟙 j)).hom = 𝟙 ((category_theory.limits.cones.postcompose (F.map (𝟙 j))).obj (c.obj j)).X) . "obviously"
- comp : (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), (c.map (f ≫ g)).hom = (c.map f).hom ≫ (c.map g).hom) . "obviously"
A structure carrying a diagram of cones over the the functors F.obj j.
def
category_theory.limits.diagram_of_cones.cone_points
{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} :
Extract the functor J ⥤ C consisting of the cone points and the maps between them,
from a diagram_of_cones.
@[simp]
theorem
category_theory.limits.diagram_of_cones.cone_points_obj
{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}
(D : category_theory.limits.diagram_of_cones F)
(j : J) :
D.cone_points.obj j = (D.obj j).X
@[simp]
theorem
category_theory.limits.diagram_of_cones.cone_points_map
{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}
(D : category_theory.limits.diagram_of_cones F)
(j j' : J)
(f : j ⟶ j') :
D.cone_points.map f = (D.map f).hom
def
category_theory.limits.cone_of_cone_uncurry
{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}
{D : category_theory.limits.diagram_of_cones F} :
(Π (j : J), category_theory.limits.is_limit (D.obj j)) → category_theory.limits.cone (category_theory.uncurry.obj F) → category_theory.limits.cone D.cone_points
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.
@[simp]
theorem
category_theory.limits.cone_of_cone_uncurry_π_app
{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}
{D : category_theory.limits.diagram_of_cones F}
(Q : Π (j : J), category_theory.limits.is_limit (D.obj j))
(c : category_theory.limits.cone (category_theory.uncurry.obj F))
(j : J) :
@[simp]
theorem
category_theory.limits.cone_of_cone_uncurry_X
{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}
{D : category_theory.limits.diagram_of_cones F}
(Q : Π (j : J), category_theory.limits.is_limit (D.obj j))
(c : category_theory.limits.cone (category_theory.uncurry.obj F)) :
def
category_theory.limits.cone_of_cone_uncurry_is_limit
{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}
{D : category_theory.limits.diagram_of_cones F}
(Q : Π (j : J), category_theory.limits.is_limit (D.obj j))
{c : category_theory.limits.cone (category_theory.uncurry.obj F)} :
cone_of_cone_uncurry Q c is a limit cone when c is a limit cone.`
def
category_theory.limits.diagram_of_cones.mk_of_has_limits
{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)
[category_theory.limits.has_limits_of_shape K C] :
Given a functor F : J ⥤ K ⥤ C, with all needed chosen limits,
we can construct a diagram consisting of the limit cone over each functor F.obj j,
and the universal cone morphisms between these.
@[simp]
theorem
category_theory.limits.diagram_of_cones.mk_of_has_limits_obj
{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)
[category_theory.limits.has_limits_of_shape K C]
(j : J) :
@[simp]
theorem
category_theory.limits.diagram_of_cones.mk_of_has_limits_map_hom
{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)
[category_theory.limits.has_limits_of_shape K C]
(j j' : J)
(f : j ⟶ j') :
@[instance]
def
category_theory.limits.diagram_of_cones_inhabited
{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)
[category_theory.limits.has_limits_of_shape K C] :
Equations
@[simp]
theorem
category_theory.limits.diagram_of_cones.mk_of_has_limits_cone_points
{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)
[category_theory.limits.has_limits_of_shape K C] :
def
category_theory.limits.limit_uncurry_iso_limit_comp_lim
{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)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit (category_theory.uncurry.obj F)]
[category_theory.limits.has_limit (F ⋙ category_theory.limits.lim)] :
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))
@[simp]
theorem
category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π
{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)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit (category_theory.uncurry.obj F)]
[category_theory.limits.has_limit (F ⋙ category_theory.limits.lim)]
{j : J}
{k : K} :
@[simp]
theorem
category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π
{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)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit (category_theory.uncurry.obj F)]
[category_theory.limits.has_limit (F ⋙ category_theory.limits.lim)]
{j : J}
{k : K} :
def
category_theory.limits.limit_iso_limit_curry_comp_lim
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(G : J × K ⥤ C)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit G]
[category_theory.limits.has_limit (category_theory.curry.obj G ⋙ category_theory.limits.lim)] :
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, _).
@[simp]
theorem
category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(G : J × K ⥤ C)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit G]
[category_theory.limits.has_limit (category_theory.curry.obj G ⋙ category_theory.limits.lim)]
{j : J}
{k : K} :
@[simp]
theorem
category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(G : J × K ⥤ C)
[category_theory.limits.has_limits_of_shape K C]
[category_theory.limits.has_limit G]
[category_theory.limits.has_limit (category_theory.curry.obj G ⋙ category_theory.limits.lim)]
{j : J}
{k : K} :