Functors which preserve κ-presentable objects #
class CategoryTheory.Functor.PreservesCardinalPresentable {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
Let F : C ⥤ D be a functor and κ be a regular cardinal, we say
that F.PreservesCardinalPresentable κ holds if for any X : C
that is κ-presentable in C, the object F.obj X is κ-presentable in D.
- le_inverseImage_isCardinalPresentable : isCardinalPresentable C κ ≤ (isCardinalPresentable D κ).inverseImage F
Instances
instance CategoryTheory.Functor.instIsCardinalPresentableObjOfPreservesCardinalPresentable {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) [IsCardinalPresentable X κ] [F.PreservesCardinalPresentable κ] :
IsCardinalPresentable (F.obj X) κ
instance CategoryTheory.Functor.instPreservesCardinalPresentableId {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] :
instance CategoryTheory.Functor.instPreservesCardinalPresentableComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.PreservesCardinalPresentable κ] [G.PreservesCardinalPresentable κ] :
(F.comp G).PreservesCardinalPresentable κ
theorem CategoryTheory.Functor.PreservesCardinalPresentable.of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} (e : F ≅ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.PreservesCardinalPresentable κ] :
theorem CategoryTheory.Functor.PreservesCardinalPresentable.iff_of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} (e : F ≅ G) (κ : Cardinal.{w}) [Fact κ.IsRegular] :