J

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

URI: https://scilib.ai/kg/mathlib#CategoryTheory.AreCardinalFilteredGenerators.J

Lean4

/-- When `G : ι → C` is a family of objects such that `AreCardinalFilteredGenerators G κ`
holds, and `X : C`, this is the index category of a presentation of `X`
as a `κ`-filtered colimit of objects in the family `G`. -/
def J : Type w :=
  (h.exists_colimitPresentation X).choose

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

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

Разделы

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

Аффилиация

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