Colimits of presentable objects #
In this file, we show that κ-accessible functors (to the category of types)
are stable under limits indexed by a category K such that
HasCardinalLT (Arrow K) κ.
In particular, κ-presentable objects are stable by colimits indexed
by a category K such that HasCardinalLT (Arrow K) κ.
theorem CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective {C : Type u} [Category.{v, u} C] {K : Type u'} [Category.{v', u'} K] {F : Functor K (Functor C (Type w'))} (c : Limits.Cone F) (hc : (Y : C) → Limits.IsLimit (((evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (Arrow K) κ) {J : Type w} [SmallCategory J] [IsCardinalFiltered J κ] {X : Functor J C} (cX : Limits.Cocone X) (hF : (k : K) → Limits.IsColimit ((F.obj k).mapCocone cX)) (x : c.pt.obj cX.pt) :
theorem CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective {C : Type u} [Category.{v, u} C] {K : Type u'} [Category.{v', u'} K] {F : Functor K (Functor C (Type w'))} (c : Limits.Cone F) (hc : (Y : C) → Limits.IsLimit (((evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (Arrow K) κ) {J : Type w} [SmallCategory J] [IsCardinalFiltered J κ] {X : Functor J C} (cX : Limits.Cocone X) (hF : (k : K) → Limits.IsColimit ((F.obj k).mapCocone cX)) (j : J) (x₁ x₂ : c.pt.obj (X.obj j)) (h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂) :
∃ (j' : J) (α : j ⟶ j'), (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂
noncomputable def CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone {C : Type u} [Category.{v, u} C] {K : Type u'} [Category.{v', u'} K] {F : Functor K (Functor C (Type w'))} (c : Limits.Cone F) (hc : (Y : C) → Limits.IsLimit (((evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (Arrow K) κ) {J : Type w} [SmallCategory J] [IsCardinalFiltered J κ] {X : Functor J C} (cX : Limits.Cocone X) (hF : (k : K) → Limits.IsColimit ((F.obj k).mapCocone cX)) :
Limits.IsColimit (c.pt.mapCocone cX)
Auxiliary definition for isCardinalAccessible_of_isLimit.
Equations
- CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone c hc κ hK cX hF = CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' (X.comp c.pt) (c.pt.mapCocone cX) ⋯ ⋯
Instances For
theorem CategoryTheory.Functor.isCardinalAccessible_of_isLimit {C : Type u} [Category.{v, u} C] {K : Type u'} [Category.{v', u'} K] {F : Functor K (Functor C (Type w'))} (c : Limits.Cone F) (hc : Limits.IsLimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasLimitsOfShape K (Type w')] (hK : HasCardinalLT (Arrow K) κ) [∀ (k : K), (F.obj k).IsCardinalAccessible κ] :
theorem CategoryTheory.isCardinalPresentable_of_isColimit' {C : Type u} [Category.{v, u} C] {K : Type u'} [Category.{v', u'} K] {Y : Functor K C} (c : Limits.Cocone Y) (hc : Limits.IsColimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasLimitsOfShape Kᵒᵖ (Type v)] (hK : HasCardinalLT (Arrow K) κ) [∀ (k : K), IsCardinalPresentable (Y.obj k) κ] :
In case C is locally w-small, use isCardinalPresentable_of_isColimit.
theorem CategoryTheory.isCardinalPresentable_of_isColimit {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {K : Type u'} [Category.{v', u'} K] [Limits.HasLimitsOfShape Kᵒᵖ (Type w)] {Y : Functor K C} (c : Limits.Cocone Y) (hc : Limits.IsColimit c) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (Arrow K) κ) [∀ (k : K), IsCardinalPresentable (Y.obj k) κ] :
theorem CategoryTheory.isClosedUnderColimitsOfShape_isCardinalPresentable (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] {J : Type u'} [Category.{v', u'} J] [Limits.HasLimitsOfShape Jᵒᵖ (Type w)] (hJ : HasCardinalLT (Arrow J) κ) :