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.
- obj : (j : J) → CategoryTheory.Limits.Cone (F.obj j)
- map : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cones.postcompose (F.map f)).obj (CategoryTheory.Limits.DiagramOfCones.obj s j) ⟶ CategoryTheory.Limits.DiagramOfCones.obj s j'
- id : ∀ (j : J), (CategoryTheory.Limits.DiagramOfCones.map s (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.Cones.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (CategoryTheory.Limits.DiagramOfCones.obj s j)).pt
- comp : ∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), (CategoryTheory.Limits.DiagramOfCones.map s (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.DiagramOfCones.map s f).hom (CategoryTheory.Limits.DiagramOfCones.map s g).hom
A structure carrying a diagram of cones over the functors F.obj j
.
Instances For
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
coneOfConeUncurry Q c
is a limit cone when c
is a limit cone.
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 limit of F.flip ⋙ lim
is isomorphic to the limit of F ⋙ lim
.
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)$.