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 ⥤ Karoubi D`. -/
@[simps!]
def functorExtension₁CompWhiskeringLeftToKaroubiIso :
    functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ≅ 𝟭 _ :=
  NatIso.ofComponents
    (fun F =>
      NatIso.ofComponents
        (fun X =>
          { hom := { f := (F.obj X).p }
            inv := { f := (F.obj X).p } })
        (fun {X Y} f => by simp))
    (by cat_disch)

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

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

Разделы

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

Аффилиация

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