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 IsPresentable.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

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] : Prop

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

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 κ] : Limits.PreservesColimitsOfShape J F

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 κ] : Limits.PreservesColimitsOfShape J F

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 κ] : G.IsCardinalAccessible κ

instance CategoryTheory.Functor.instIsCardinalAccessibleId {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (Functor.id C).IsCardinalAccessible κ

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] : F.IsCardinalAccessible κ

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

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 κ

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 κ] : IsAccessible.{w, v₁, v₂, u₁, u₂} F

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] : IsAccessible.{w, v₁, v₃, u₁, u₃} (F.comp 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] : Prop

An object X in a category is κ-presentable (for κ a regular cardinal) when the functor Hom(X, _) preserves colimits indexed by κ-filtered categories.

Equations

• CategoryTheory.IsCardinalPresentable X κ = (CategoryTheory.coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ

@[reducible, inline]

abbrev CategoryTheory.isCardinalPresentable (C : Type u₁) [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : ObjectProperty C

The property of objects that are κ-presentable.

Equations

• CategoryTheory.isCardinalPresentable C κ X = CategoryTheory.IsCardinalPresentable X κ

instance CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : (isCardinalPresentable C κ).FullSubcategory) : IsCardinalPresentable X.obj κ

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] : IsCardinalPresentable X κ ↔ (coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ

theorem CategoryTheory.isCardinalPresentable_iff {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) : isCardinalPresentable C κ X ↔ IsCardinalPresentable X κ

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 κ] : Limits.PreservesColimitsOfShape J (coyoneda.obj (Opposite.op X))

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 κ] : Limits.PreservesColimitsOfShape J (coyoneda.obj (Opposite.op X))

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 : κ ≤ κ') : IsCardinalPresentable X κ'

theorem CategoryTheory.isCardinalPresentable_monotone (C : Type u₁) [Category.{v₁, u₁} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : isCardinalPresentable C κ ≤ isCardinalPresentable C κ'

theorem CategoryTheory.isCardinalPresentable_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : IsCardinalPresentable Y κ

instance CategoryTheory.instIsClosedUnderIsomorphismsIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms

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] : IsCardinalPresentable (F.obj X) κ ↔ IsCardinalPresentable X κ

theorem CategoryTheory.IsCardinalPresentable.mk {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {κ : Cardinal.{w}} [Fact κ.IsRegular] (hX : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ] (F : Functor J C) (c : Limits.Cocone F) (x : Limits.IsColimit c), (∀ (g : X ⟶ c.pt), ∃ (j : J) (f : X ⟶ F.obj j), CategoryStruct.comp f (c.ι.app j) = g) ∧ ∀ (j : J) (f₁ f₂ : X ⟶ F.obj j), CategoryStruct.comp f₁ (c.ι.app j) = CategoryStruct.comp f₂ (c.ι.app j) → ∃ (j' : J) (a : j ⟶ j'), CategoryStruct.comp f₁ (F.map a) = CategoryStruct.comp f₂ (F.map a)) : IsCardinalPresentable X κ

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) : ∃ (j : J) (p : X ⟶ D.obj j), CategoryStruct.comp p (c.ι.app j) = f

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} [IsFiltered J] {c : Cocone D} (hc : IsColimit c) {X : C} [PreservesColimit D (coyoneda.obj (Opposite.op X))] (f g : X ⟶ c.pt) : ∃ (j : J) (p : X ⟶ D.obj j) (q : X ⟶ D.obj j), CategoryStruct.comp p (c.ι.app j) = f ∧ CategoryStruct.comp q (c.ι.app j) = g

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) : ∃ (j : J) (p : D.obj j ⟶ X), CategoryStruct.comp (c.π.app j) p = f

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) : ∃ (j : J) (f' : X ⟶ F.obj j), CategoryStruct.comp f' (c.ι.app j) = f

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 g : X ⟶ c.pt) : ∃ (j : J) (f' : X ⟶ F.obj j) (g' : X ⟶ F.obj j), CategoryStruct.comp f' (c.ι.app j) = f ∧ CategoryStruct.comp g' (c.ι.app j) = g

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.exists_commSq_of_isColimit {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] {J : Type u_2} [Category.{v_2, u_2} J] [EssentiallySmall.{w, v_2, u_2} J] [IsCardinalFiltered J κ] {X Y : Functor J C} (f : X ⟶ Y) {c₁ : Limits.Cocone X} {c₂ : Limits.Cocone Y} (hc₁ : Limits.IsColimit c₁) (hc₂ : Limits.IsColimit c₂) (f' : c₁.pt ⟶ c₂.pt) (hf' : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f' = CategoryStruct.comp (f.app j) (c₂.ι.app j)) ⦃X' Y' : C⦄ ⦃t : X' ⟶ Y'⦄ ⦃l : X' ⟶ c₁.pt⦄ ⦃r : Y' ⟶ c₂.pt⦄ [IsCardinalPresentable X' κ] [IsCardinalPresentable Y' κ] (sq : CommSq t l r f') : ∃ (j : J) (l' : X' ⟶ X.obj j) (r' : Y' ⟶ Y.obj j), CategoryStruct.comp l' (c₁.ι.app j) = l ∧ CategoryStruct.comp r' (c₂.ι.app j) = r ∧ CommSq t l' r' (f.app j)

Given a commutative square where both objects on the top are κ-presentable and the bottom map is a colimit of a natural transformation f : X ⟶ Y between functors in J ⥤ C where J is κ-filtered, the commutative square can be refined by replacing the colimit map in the bottom by a morphism f.app j : X.obj j ⟶ Y.obj j for a big enough j.

theorem CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : IsCardinalPresentable X κ ↔ (uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ

instance CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : (uliftCoyoneda.{t, v₁, u₁}.obj (Opposite.op X)).IsCardinalAccessible κ

@[reducible, inline]

abbrev CategoryTheory.IsPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Prop

An object of a category is presentable relative to a universe w if it is κ-presentable for some regular κ : Cardinal.{w}.

Equations

• CategoryTheory.IsPresentable.{?u.3, ?u.2, ?u.1} X = CategoryTheory.Functor.IsAccessible.{?u.3, ?u.2, ?u.2, ?u.1, ?u.2 + 1} (CategoryTheory.coyoneda.obj (Opposite.op X))

theorem CategoryTheory.isPresentable_of_isCardinalPresentable {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] : IsPresentable.{w, v₁, u₁} X

class CategoryTheory.HasCardinalFilteredColimits (C : Type u₁) [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop

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

instance CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [Limits.HasColimitsOfSize.{w, w, v₁, u₁} C] : HasCardinalFilteredColimits C κ

theorem CategoryTheory.HasCardinalFilteredColimits.of_le {C : Type u₁} [Category.{v₁, u₁} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [HasCardinalFilteredColimits C κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : HasCardinalFilteredColimits C κ'