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 : c.pt.map (cX.ι.app j) x₁ = c.pt.map (cX.ι.app j) 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) κ]
: