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