reindex

Mathlib.CategoryTheory.Limits.Presentation

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.ColimitPresentation.reindex

Lean4

/-- Change the index category of a colimit presentation. -/
@[simps]
noncomputable def reindex (P : ColimitPresentation J X) {J' : Type*} [Category J'] (F : J' ⥤ J) [F.Final] :
    ColimitPresentation J' X where
  diag := F ⋙ P.diag
  ι := F.whiskerLeft P.ι
  isColimit := (Functor.Final.isColimitWhiskerEquiv F _).symm P.isColimit

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

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

Разделы

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

Аффилиация

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