functorExtension₂CompWhiskeringLeftToKaroubiIso

Mathlib.CategoryTheory.Idempotents.FunctorExtension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso

Lean4

/-- The natural isomorphism expressing that functors `Karoubi C ⥤ Karoubi D` obtained
using `functorExtension₂` actually extends the original functors `C ⥤ D`. -/
@[simps!]
def functorExtension₂CompWhiskeringLeftToKaroubiIso :
    functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ≅
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) :=
  NatIso.ofComponents
    (fun F =>
      NatIso.ofComponents
        (fun X =>
          { hom := { f := 𝟙 _ }
            inv := { f := 𝟙 _ } })
        (by simp))
    (by cat_disch)

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

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

Разделы

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

Аффилиация

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