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) κ)
: