mathlib3 documentation

category_theory.limits.fubini

A Fubini theorem for categorical limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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 functors F.obj j.

Instances for category_theory.limits.diagram_of_cones
source
@[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
source
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} (D : category_theory.limits.diagram_of_cones F) :
J ⥤ C

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

Equations
source
@[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
source
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} (Q : Π (j : J), category_theory.limits.is_limit (D.obj j)) (c : 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.

Equations
source
@[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) :
(category_theory.limits.cone_of_cone_uncurry Q c).π.app j = (Q j).lift {X := c.X, π := {app := λ (k : K), c.π.app (j, k), naturality' := _}}
source
@[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)) :
(category_theory.limits.cone_of_cone_uncurry Q c).X = c.X
source
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)} (P : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.limits.cone_of_cone_uncurry Q c)

cone_of_cone_uncurry Q c is a limit cone when c is a limit cone.`

Equations
source
noncomputable 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] :
category_theory.limits.diagram_of_cones F

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
source
@[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) :
(category_theory.limits.diagram_of_cones.mk_of_has_limits F).obj j = category_theory.limits.limit.cone (F.obj j)
source
@[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') :
((category_theory.limits.diagram_of_cones.mk_of_has_limits F).map f).hom = category_theory.limits.lim.map (F.map f)
source
@[protected, instance]
noncomputable 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] :
inhabited (category_theory.limits.diagram_of_cones F)
Equations
source
@[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] :
(category_theory.limits.diagram_of_cones.mk_of_has_limits F).cone_points = F ⋙ category_theory.limits.lim
source
noncomputable 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)] :
category_theory.limits.limit (category_theory.uncurry.obj F) ≅ category_theory.limits.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
source
@[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} :
(category_theory.limits.limit_uncurry_iso_limit_comp_lim F).hom ≫ category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k = category_theory.limits.limit.π (category_theory.uncurry.obj F) (j, k)
source
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π_assoc {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} {X' : C} (f' : (F.obj j).obj k ⟶ X') :
(category_theory.limits.limit_uncurry_iso_limit_comp_lim F).hom ≫ category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k ≫ f' = category_theory.limits.limit.π (category_theory.uncurry.obj F) (j, k) ≫ f'
source
@[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} :
(category_theory.limits.limit_uncurry_iso_limit_comp_lim F).inv ≫ category_theory.limits.limit.π (category_theory.uncurry.obj F) (j, k) = category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k
source
@[simp]
theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π_assoc {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} {X' : C} (f' : (category_theory.uncurry.obj F).obj (j, k) ⟶ X') :
(category_theory.limits.limit_uncurry_iso_limit_comp_lim F).inv ≫ category_theory.limits.limit.π (category_theory.uncurry.obj F) (j, k) ≫ f' = category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k ≫ f'
source
noncomputable def category_theory.limits.limit_flip_comp_lim_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 J C] [category_theory.limits.has_limits_of_shape K C] [category_theory.limits.has_limits_of_shape (J × K) C] [category_theory.limits.has_limits_of_shape (K × J) C] :
category_theory.limits.limit (F.flip ⋙ category_theory.limits.lim) ≅ category_theory.limits.limit (F ⋙ category_theory.limits.lim)

The limit of F.flip ⋙ lim is isomorphic to the limit of F ⋙ lim.

Equations
source
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_hom_π_π_assoc {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 J C] [category_theory.limits.has_limits_of_shape K C] [category_theory.limits.has_limits_of_shape (J × K) C] [category_theory.limits.has_limits_of_shape (K × J) C] (j : J) (k : K) {X' : C} (f' : (F.obj j).obj k ⟶ X') :
(category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim F).hom ≫ category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k ≫ f' = category_theory.limits.limit.π (F.flip ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π (F.flip.obj k) j ≫ f'
source
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_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 J C] [category_theory.limits.has_limits_of_shape K C] [category_theory.limits.has_limits_of_shape (J × K) C] [category_theory.limits.has_limits_of_shape (K × J) C] (j : J) (k : K) :
(category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim F).hom ≫ category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k = category_theory.limits.limit.π (F.flip ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π (F.flip.obj k) j
source
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_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 J C] [category_theory.limits.has_limits_of_shape K C] [category_theory.limits.has_limits_of_shape (J × K) C] [category_theory.limits.has_limits_of_shape (K × J) C] (k : K) (j : J) :
(category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim F).inv ≫ category_theory.limits.limit.π (F.flip ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π (F.flip.obj k) j = category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k
source
@[simp]
theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_inv_π_π_assoc {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 J C] [category_theory.limits.has_limits_of_shape K C] [category_theory.limits.has_limits_of_shape (J × K) C] [category_theory.limits.has_limits_of_shape (K × J) C] (k : K) (j : J) {X' : C} (f' : (F.flip.obj k).obj j ⟶ X') :
(category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim F).inv ≫ category_theory.limits.limit.π (F.flip ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π (F.flip.obj k) j ≫ f' = category_theory.limits.limit.π (F ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π (F.obj j) k ≫ f'
source
noncomputable 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)] :
category_theory.limits.limit G ≅ category_theory.limits.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, _).

Equations
source
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π_assoc {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} {X' : C} (f' : ((category_theory.curry.obj G).obj j).obj k ⟶ X') :
(category_theory.limits.limit_iso_limit_curry_comp_lim G).hom ≫ category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k ≫ f' = category_theory.limits.limit.π G (j, k) ≫ f'
source
@[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} :
(category_theory.limits.limit_iso_limit_curry_comp_lim G).hom ≫ category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k = category_theory.limits.limit.π G (j, k)
source
@[simp]
theorem category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π_assoc {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} {X' : C} (f' : G.obj (j, k) ⟶ X') :
(category_theory.limits.limit_iso_limit_curry_comp_lim G).inv ≫ category_theory.limits.limit.π G (j, k) ≫ f' = category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k ≫ f'
source
@[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} :
(category_theory.limits.limit_iso_limit_curry_comp_lim G).inv ≫ category_theory.limits.limit.π G (j, k) = category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k
source
noncomputable def category_theory.limits.limit_curry_swap_comp_lim_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 C] :
category_theory.limits.limit (category_theory.curry.obj (category_theory.prod.swap K J ⋙ G) ⋙ category_theory.limits.lim) ≅ category_theory.limits.limit (category_theory.curry.obj G ⋙ category_theory.limits.lim)

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
source
@[simp]
theorem category_theory.limits.limit_curry_swap_comp_lim_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 C] {j : J} {k : K} :
(category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim G).hom ≫ category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k = category_theory.limits.limit.π (category_theory.curry.obj (category_theory.prod.swap K J ⋙ G) ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ G)).obj k) j
source
@[simp]
theorem category_theory.limits.limit_curry_swap_comp_lim_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 C] {j : J} {k : K} :
(category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim G).inv ≫ category_theory.limits.limit.π (category_theory.curry.obj (category_theory.prod.swap K J ⋙ G) ⋙ category_theory.limits.lim) k ≫ category_theory.limits.limit.π ((category_theory.curry.obj (category_theory.prod.swap K J ⋙ G)).obj k) j = category_theory.limits.limit.π (category_theory.curry.obj G ⋙ category_theory.limits.lim) j ≫ category_theory.limits.limit.π ((category_theory.curry.obj G).obj j) k