instIsAccessibleCategoryOfIsLocallyPresentable

Mathlib.CategoryTheory.Presentable.LocallyPresentable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsAccessibleCategoryOfIsLocallyPresentable

← MathLib Explorer

English

If C is locally presentable, then C is an accessible category.

Русский

Если C локально.presentable, то C является доступной категорией.

LaTeX

$$$\mathrm{IsAccessibleCategory}(C)$$$

Lean4

instance [IsLocallyPresentable.{w} C] : IsAccessibleCategory.{w} C where
  exists_cardinal := by
    obtain ⟨κ, hκ, h'⟩ := IsLocallyPresentable.exists_cardinal C
    exact ⟨κ, hκ, inferInstance⟩

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

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

Разделы

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

Аффилиация

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