IsFinitelyAccessible

Mathlib.CategoryTheory.Presentable.Finite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsFinitelyAccessible

Lean4

/-- A functor `F : C ⥤ D` is finitely accessible if it is `ℵ₀`-accessible.
Equivalently, it preserves all filtered colimits.
See `CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimits`. -/
abbrev IsFinitelyAccessible (F : C ⥤ D) : Prop :=
  IsCardinalAccessible.{w} F ℵ₀

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru