Structures · Category theory
CategoryTheory.Functor.IsCardinalAccessible
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
- Shape
- 2 explicit arguments · adds preservesColimitOfShape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
- CategoryTheory.Adjunction.hasCardinalFilteredGenerator
- CategoryTheory.Functor.isCardinalAccessible_of_natIso
- CategoryTheory.Adjunction.isCardinalLocallyPresentable
- CategoryTheory.Functor.isCardinalAccessible_of_isLimit
- CategoryTheory.Adjunction.isCardinalPresentable_leftAdjoint_obj
- CategoryTheory.Functor.isCardinalAccessible_of_le
- CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape
- CategoryTheory.Adjunction.isCardinalFilteredGenerator
- CategoryTheory.Adjunction.isCardinalAccessibleCategory
- CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall
- CategoryTheory.Functor.instIsCardinalAccessibleComp
- CategoryTheory.Functor.isAccessible_of_isCardinalAccessible
Ancestors0
No ancestors.