Presentable objects #
A functor F : C ⥤ D is κ-accessible (Functor.IsCardinalAccessible)
if it commutes with colimits of shape J where J is any κ-filtered category
(that is essentially small relative to the universe w such that κ : Cardinal.{w}.).
We also introduce another typeclass Functor.IsAccessible saying that there exists
a regular cardinal κ such that Functor.IsCardinalAccessible.
An object X of a category is κ-presentable (IsCardinalPresentable)
if the functor Hom(X, _) (i.e. coyoneda.obj (op X)) is κ-accessible.
Similarly as for accessible functors, we define a type class IsAccessible.
References #
class
CategoryTheory.Functor.IsCardinalAccessible
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
A functor F : C ⥤ D is κ-accessible (with κ a regular cardinal)
if it preserves colimits of shape J where J is any κ-filtered category.
In the mathematical literature, some assumptions are often made on the
categories C or D (e.g. the existence of κ-filtered colimits,
see HasCardinalFilteredColimits below), but here we do not
make such assumptions.
- preservesColimitOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.PreservesColimitsOfShape J F
Instances
theorem
CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F.IsCardinalAccessible κ]
(J : Type w)
[SmallCategory J]
[IsCardinalFiltered J κ]
:
theorem
CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F.IsCardinalAccessible κ]
(J : Type u₃)
[Category.{v₃, u₃} J]
[EssentiallySmall.{w, v₃, u₃} J]
[IsCardinalFiltered J κ]
:
theorem
CategoryTheory.Functor.isCardinalAccessible_of_le
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
[F.IsCardinalAccessible κ]
{κ' : Cardinal.{w}}
[Fact κ'.IsRegular]
(h : κ ≤ κ')
:
F.IsCardinalAccessible κ'
theorem
CategoryTheory.Functor.isCardinalAccessible_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(e : F ≅ G)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F.IsCardinalAccessible κ]
:
instance
CategoryTheory.Functor.instIsCardinalAccessibleId
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
instance
CategoryTheory.Functor.instIsCardinalAccessibleComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsCardinalAccessible κ]
[G.IsCardinalAccessible κ]
:
(F.comp G).IsCardinalAccessible κ
instance
CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[Limits.PreservesColimitsOfSize.{w, w, v₁, v₂, u₁, u₂} F]
:
instance
CategoryTheory.Functor.instIsCardinalAccessibleObjConst
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
(A : C)
:
((const C).obj A).IsCardinalAccessible κ
class
CategoryTheory.Functor.IsAccessible
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor is accessible relative to a universe w if
it is κ-accessible for some regular κ : Cardinal.{w}.
- exists_cardinal : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), F.IsCardinalAccessible κ
Instances
theorem
CategoryTheory.Functor.isAccessible_of_isCardinalAccessible
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F.IsCardinalAccessible κ]
:
instance
CategoryTheory.Functor.instIsAccessibleComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[IsAccessible.{w, v₁, v₂, u₁, u₂} F]
[IsAccessible.{w, v₂, v₃, u₂, u₃} G]
:
instance
CategoryTheory.Functor.instIsAccessibleObjConst
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : C)
:
IsAccessible.{w, v₁, v₁, u₁, u₁} ((const C).obj A)
@[reducible, inline]
abbrev
CategoryTheory.IsCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
An object X in a category is κ-presentable (for κ a regular cardinal)
when the functor Hom(X, _) preserves colimits indexed by
κ-filtered categories.
Equations
Instances For
def
CategoryTheory.isCardinalPresentable
(C : Type u₁)
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
The property of objects that are κ-presentable.
Equations
Instances For
instance
CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
(X : (isCardinalPresentable C κ).FullSubcategory)
:
instance
CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
(X : (isCardinalPresentable C κ).FullSubcategory)
:
IsCardinalPresentable ((isCardinalPresentable C κ).ι.obj X) κ
theorem
CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
theorem
CategoryTheory.isCardinalPresentable_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
(X : C)
:
theorem
CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
(J : Type w)
[SmallCategory J]
[IsCardinalFiltered J κ]
:
theorem
CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
(J : Type u₃)
[Category.{v₃, u₃} J]
[EssentiallySmall.{w, v₃, u₃} J]
[IsCardinalFiltered J κ]
:
theorem
CategoryTheory.isCardinalPresentable_of_le
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
{κ' : Cardinal.{w}}
[Fact κ'.IsRegular]
(h : κ ≤ κ')
:
theorem
CategoryTheory.isCardinalPresentable_monotone
(C : Type u₁)
[Category.{v₁, u₁} C]
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
{κ' : Cardinal.{w}}
[Fact κ'.IsRegular]
(h : κ ≤ κ')
:
theorem
CategoryTheory.isCardinalPresentable_of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
(e : X ≅ Y)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
:
instance
CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
theorem
CategoryTheory.isCardinalPresentable_of_equivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{C' : Type u₃}
[Category.{v₃, u₃} C']
[IsCardinalPresentable X κ]
(e : C ≌ C')
:
IsCardinalPresentable (e.functor.obj X) κ
instance
CategoryTheory.isCardinalPresentable_of_isEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{C' : Type u₃}
[Category.{v₃, u₃} C']
[IsCardinalPresentable X κ]
(F : Functor C C')
[F.IsEquivalence]
:
IsCardinalPresentable (F.obj X) κ
@[simp]
theorem
CategoryTheory.isCardinalPresentable_iff_of_isEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{C' : Type u₃}
[Category.{v₃, u₃} C']
(F : Functor C C')
[F.IsEquivalence]
:
theorem
CategoryTheory.Limits.exists_hom_of_preservesColimit_coyoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
{c : Cocone D}
(hc : IsColimit c)
{X : C}
[PreservesColimit D (coyoneda.obj (Opposite.op X))]
(f : X ⟶ c.pt)
:
theorem
CategoryTheory.Limits.exists_eq_of_preservesColimit_coyoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
[IsFiltered J]
{c : Cocone D}
(hc : IsColimit c)
{X : C}
[PreservesColimit D (coyoneda.obj (Opposite.op X))]
{i j : J}
(f : X ⟶ D.obj i)
(g : X ⟶ D.obj j)
(h : CategoryStruct.comp f (c.ι.app i) = CategoryStruct.comp g (c.ι.app j))
:
∃ (k : J) (u : i ⟶ k) (v : j ⟶ k), CategoryStruct.comp f (D.map u) = CategoryStruct.comp g (D.map v)
theorem
CategoryTheory.Limits.exists_eq_of_preservesColimit_coyoneda_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
[IsFiltered J]
{c : Cocone D}
(hc : IsColimit c)
{X : C}
[PreservesColimit D (coyoneda.obj (Opposite.op X))]
{i : J}
(f g : X ⟶ D.obj i)
(h : CategoryStruct.comp f (c.ι.app i) = CategoryStruct.comp g (c.ι.app i))
:
∃ (j : J) (a : i ⟶ j), CategoryStruct.comp f (D.map a) = CategoryStruct.comp g (D.map a)
theorem
CategoryTheory.Limits.exists_hom_of_preservesColimit_yoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
{c : Cone D}
(hc : IsLimit c)
{X : C}
[PreservesColimit D.op (yoneda.obj X)]
(f : c.pt ⟶ X)
:
theorem
CategoryTheory.Limits.exists_eq_of_preservesColimit_yoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
[IsCofiltered J]
{c : Cone D}
(hc : IsLimit c)
{X : C}
[PreservesColimit D.op (yoneda.obj X)]
{i j : J}
(f : D.obj i ⟶ X)
(g : D.obj j ⟶ X)
(h : CategoryStruct.comp (c.π.app i) f = CategoryStruct.comp (c.π.app j) g)
:
∃ (k : J) (u : k ⟶ i) (v : k ⟶ j), CategoryStruct.comp (D.map u) f = CategoryStruct.comp (D.map v) g
theorem
CategoryTheory.Limits.exists_eq_of_preservesColimit_yoneda_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u_1}
[Category.{v_1, u_1} J]
{D : Functor J C}
[IsCofiltered J]
{c : Cone D}
(hc : IsLimit c)
{X : C}
[PreservesColimit D.op (yoneda.obj X)]
{i : J}
(f g : D.obj i ⟶ X)
(h : CategoryStruct.comp (c.π.app i) f = CategoryStruct.comp (c.π.app i) g)
:
∃ (j : J) (a : j ⟶ i), CategoryStruct.comp (D.map a) f = CategoryStruct.comp (D.map a) g
theorem
CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{J : Type u_1}
[Category.{v_1, u_1} J]
[IsCardinalPresentable X κ]
[EssentiallySmall.{w, v_1, u_1} J]
[IsCardinalFiltered J κ]
{F : Functor J C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
(f : X ⟶ c.pt)
:
theorem
CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{J : Type u_1}
[Category.{v_1, u_1} J]
[IsCardinalPresentable X κ]
[EssentiallySmall.{w, v_1, u_1} J]
[IsCardinalFiltered J κ]
{F : Functor J C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
{i₁ i₂ : J}
(f₁ : X ⟶ F.obj i₁)
(f₂ : X ⟶ F.obj i₂)
(hf : CategoryStruct.comp f₁ (c.ι.app i₁) = CategoryStruct.comp f₂ (c.ι.app i₂))
:
∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), CategoryStruct.comp f₁ (F.map u) = CategoryStruct.comp f₂ (F.map v)
theorem
CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
(κ : Cardinal.{w})
[Fact κ.IsRegular]
{J : Type u_1}
[Category.{v_1, u_1} J]
[IsCardinalPresentable X κ]
[EssentiallySmall.{w, v_1, u_1} J]
[IsCardinalFiltered J κ]
{F : Functor J C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
{i : J}
(f₁ f₂ : X ⟶ F.obj i)
(hf : CategoryStruct.comp f₁ (c.ι.app i) = CategoryStruct.comp f₂ (c.ι.app i))
:
∃ (j : J) (u : i ⟶ j), CategoryStruct.comp f₁ (F.map u) = CategoryStruct.comp f₂ (F.map u)
theorem
CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
instance
CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
:
@[reducible, inline]
An object of a category is presentable relative to a universe w
if it is κ-presentable for some regular κ : Cardinal.{w}.
Equations
Instances For
theorem
CategoryTheory.isPresentable_of_isCardinalPresentable
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : C)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalPresentable X κ]
:
class
CategoryTheory.HasCardinalFilteredColimits
(C : Type u₁)
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
A category has κ-filtered colimits if it has colimits of shape J
for any κ-filtered category J.
- hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : Limits.HasColimitsOfShape J C
Instances
instance
CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize
(C : Type u₁)
[Category.{v₁, u₁} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[Limits.HasColimitsOfSize.{w, w, v₁, u₁} C]
: