Colimits on Grothendieck constructions preserving limits #
We characterize the condition in which colimits on Grothendieck constructions preserve limits: By preserving limits on the Grothendieck construction's base category as well as on each of its fibers.
def
CategoryTheory.Limits.fiberwiseColimitLimitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{H : Type u₂}
[Category.{v₂, u₂} H]
{J : Type u₃}
[Category.{v₃, u₃} J]
{F : Functor C Cat}
(K : Functor J (Functor (Grothendieck F) H))
[∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H]
[HasLimitsOfShape J H]
[∀ (c : C), PreservesLimitsOfShape J colim]
:
fiberwiseColimit (limit K) ≅ limit (K.comp (fiberwiseColim F H))
If colim on each fiber F.obj c of a functor F : C ⥤ Cat preserves limits of shape J,
then the fiberwise colimit of the limit of a functor K : J ⥤ Grothendieck F ⥤ H is naturally
isomorphic to taking the limit of the composition K ⋙ fiberwiseColim F H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{H : Type u₂}
[Category.{v₂, u₂} H]
{J : Type u₃}
[Category.{v₃, u₃} J]
{F : Functor C Cat}
(K : Functor J (Functor (Grothendieck F) H))
[∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H]
[HasLimitsOfShape J H]
[∀ (c : C), PreservesLimitsOfShape J colim]
(X : C)
:
(fiberwiseColimitLimitIso K).inv.app X = CategoryStruct.comp (limitObjIsoLimitCompEvaluation (K.comp (fiberwiseColim F H)) X).hom
(CategoryStruct.comp
(HasLimit.isoOfNatIso
(K.associator ((whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)) colim ≪≫ isoWhiskerLeft K (fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (fiberwiseColim F H) ((evaluation C H).obj X)).symm)).inv
(CategoryStruct.comp
(preservesLimitIso colim
(K.comp ((whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)))).inv
(HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F X)).symm).inv))
@[simp]
theorem
CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{H : Type u₂}
[Category.{v₂, u₂} H]
{J : Type u₃}
[Category.{v₃, u₃} J]
{F : Functor C Cat}
(K : Functor J (Functor (Grothendieck F) H))
[∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H]
[HasLimitsOfShape J H]
[∀ (c : C), PreservesLimitsOfShape J colim]
(X : C)
:
(fiberwiseColimitLimitIso K).hom.app X = CategoryStruct.comp (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F X)).symm).hom
(CategoryStruct.comp
(preservesLimitIso colim (K.comp ((whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)))).hom
(CategoryStruct.comp
(HasLimit.isoOfNatIso
(K.associator ((whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)) colim ≪≫ isoWhiskerLeft K (fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (fiberwiseColim F H) ((evaluation C H).obj X)).symm)).hom
(limitObjIsoLimitCompEvaluation (K.comp (fiberwiseColim F H)) X).inv))
instance
CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck
(C : Type u₁)
[Category.{v₁, u₁} C]
{H : Type u₂}
[Category.{v₂, u₂} H]
{J : Type u₃}
[Category.{v₃, u₃} J]
(F : Functor C Cat)
[HasColimitsOfShape C H]
[HasLimitsOfShape J H]
[∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H]
[PreservesLimitsOfShape J colim]
[∀ (c : C), PreservesLimitsOfShape J colim]
:
If colim on a category C preserves limits of shape J and if it does so for colim on
every F.obj c for a functor F : C ⥤ Cat, then colim on Grothendieck F also preserves limits
of shape J.