Theorems · Inductive type · category theory

CategoryTheory.Functor.IsCardinalAccessible

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Presentable.Basic

Cited by

19 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFact