functorExtension₁Comp

Mathlib.CategoryTheory.Idempotents.FunctorExtension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.functorExtension₁Comp

Lean4

/-- Compatibility isomorphisms of `functorExtension₁` with respect to the
composition of functors. -/
def functorExtension₁Comp (F : C ⥤ Karoubi D) (G : D ⥤ Karoubi E) :
    (functorExtension₁ C E).obj (F ⋙ (functorExtension₁ D E).obj G) ≅
      (functorExtension₁ C D).obj F ⋙ (functorExtension₁ D E).obj G :=
  Iso.refl _

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

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

Разделы

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

Аффилиация

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