colimitPresentation

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

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

Lean4

/-- A choice of a presentation of an object `X` in a category `C`
as a `κ`-filtered colimit of objects in the family `G : ι → C`
when `h : AreCardinalFilteredGenerators G κ`. -/
noncomputable def colimitPresentation : ColimitPresentation (h.J X) X :=
  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose_spec.choose

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

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

Разделы

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

Аффилиация

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