Extension of functors to the idempotent completion

In this file, we construct an extension functorExtension₁ of functors C ⥤ Karoubi D to functors Karoubi C ⥤ Karoubi D. This results in an equivalence karoubiUniversal₁ C D : (C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D).

We also construct an extension functorExtension₂ of functors (C ⥤ D) ⥤ (Karoubi C ⥤ Karoubi D). Moreover, when D is idempotent complete, we get equivalences karoubiUniversal₂ C D : C ⥤ D ≌ Karoubi C ⥤ Karoubi D and karoubiUniversal C D : C ⥤ D ≌ Karoubi C ⥤ D.

theorem CategoryTheory.Idempotents.natTrans_eq {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F G : Functor (Karoubi C) D} (φ : F ⟶ G) (P : Karoubi C) : φ.app P = CategoryStruct.comp (F.map P.decompId_i) (CategoryStruct.comp (φ.app { X := P.X, p := CategoryStruct.id P.X, idem := ⋯ }) (G.map P.decompId_p))

A natural transformation between functors Karoubi C ⥤ D is determined by its value on objects coming from C.

def CategoryTheory.Idempotents.FunctorExtension₁.obj {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C (Karoubi D)) : Functor (Karoubi C) (Karoubi D)

The canonical extension of a functor C ⥤ Karoubi D to a functor Karoubi C ⥤ Karoubi D

@[simp]

theorem CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C (Karoubi D)) (P : Karoubi C) : ((obj F).obj P).p = (F.map P.p).f

@[simp]

theorem CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_X {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C (Karoubi D)) (P : Karoubi C) : ((obj F).obj P).X = (F.obj P.X).X

@[simp]

theorem CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C (Karoubi D)) {X✝ Y✝ : Karoubi C} (f : X✝ ⟶ Y✝) : ((obj F).map f).f = (F.map f.f).f

def CategoryTheory.Idempotents.FunctorExtension₁.map {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F G : Functor C (Karoubi D)} (φ : F ⟶ G) : obj F ⟶ obj G

Extension of a natural transformation φ between functors C ⥤ karoubi D to a natural transformation between the extension of these functors to karoubi C ⥤ karoubi D

@[simp]

theorem CategoryTheory.Idempotents.FunctorExtension₁.map_app_f {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {F G : Functor C (Karoubi D)} (φ : F ⟶ G) (P : Karoubi C) : ((map φ).app P).f = CategoryStruct.comp (F.map P.p).f (φ.app P.X).f

def CategoryTheory.Idempotents.functorExtension₁ (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : Functor (Functor C (Karoubi D)) (Functor (Karoubi C) (Karoubi D))

The canonical functor (C ⥤ Karoubi D) ⥤ (Karoubi C ⥤ Karoubi D)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₁_obj (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (F : Functor C (Karoubi D)) : (functorExtension₁ C D).obj F = FunctorExtension₁.obj F

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₁_map (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {X✝ Y✝ : Functor C (Karoubi D)} (φ : X✝ ⟶ Y✝) : (functorExtension₁ C D).map φ = FunctorExtension₁.map φ

def CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (functorExtension₁ C D).comp ((Functor.whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)) ≅ Functor.id (Functor C (Karoubi D))

The natural isomorphism expressing that functors Karoubi C ⥤ Karoubi D obtained using functorExtension₁ actually extends the original functors C ⥤ Karoubi D.

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C (Karoubi D)) (X✝ : C) : (((functorExtension₁CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X✝).f = (X.obj X✝).p

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C (Karoubi D)) (X✝ : C) : (((functorExtension₁CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X✝).f = (X.obj X✝).p

def CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : ((Functor.whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).comp (functorExtension₁ C D) ≅ Functor.id (Functor (Karoubi C) (Karoubi D))

The counit isomorphism of the equivalence (C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D).

@[simp]

theorem CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor (Karoubi C) (Karoubi D)) (P : Karoubi C) : (((counitIso C D).inv.app X).app P).f = (X.map P.decompId_i).f

@[simp]

theorem CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor (Karoubi C) (Karoubi D)) (P : Karoubi C) : (((counitIso C D).hom.app X).app P).f = (X.map P.decompId_p).f

def CategoryTheory.Idempotents.karoubiUniversal₁ (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : Functor C (Karoubi D) ≌ Functor (Karoubi C) (Karoubi D)

The equivalence of categories (C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D).

@[simp]

theorem CategoryTheory.Idempotents.karoubiUniversal₁_unitIso (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (karoubiUniversal₁ C D).unitIso = (functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm

@[simp]

theorem CategoryTheory.Idempotents.karoubiUniversal₁_counitIso (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (karoubiUniversal₁ C D).counitIso = KaroubiUniversal₁.counitIso C D

@[simp]

theorem CategoryTheory.Idempotents.karoubiUniversal₁_inverse (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (karoubiUniversal₁ C D).inverse = (Functor.whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)

@[simp]

theorem CategoryTheory.Idempotents.karoubiUniversal₁_functor (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (karoubiUniversal₁ C D).functor = functorExtension₁ C D

def CategoryTheory.Idempotents.functorExtension₁Comp (C : Type u_1) (D : Type u_2) (E : Type u_3) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] (F : Functor C (Karoubi D)) (G : Functor D (Karoubi E)) : (functorExtension₁ C E).obj (F.comp ((functorExtension₁ D E).obj G)) ≅ ((functorExtension₁ C D).obj F).comp ((functorExtension₁ D E).obj G)

Compatibility isomorphisms of functorExtension₁ with respect to the composition of functors.

def CategoryTheory.Idempotents.functorExtension₂ (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : Functor (Functor C D) (Functor (Karoubi C) (Karoubi D))

The canonical functor (C ⥤ D) ⥤ (Karoubi C ⥤ Karoubi D)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂_obj_map_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C D) {X✝ Y✝ : Karoubi C} (f : X✝ ⟶ Y✝) : (((functorExtension₂ C D).obj X).map f).f = X.map f.f

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂_obj_obj_p (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C D) (P : Karoubi C) : (((functorExtension₂ C D).obj X).obj P).p = X.map P.p

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂_map_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {X✝ Y✝ : Functor C D} (f : X✝ ⟶ Y✝) (P : Karoubi C) : (((functorExtension₂ C D).map f).app P).f = CategoryStruct.comp (f.app P.X) (Y✝.map P.p)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂_obj_obj_X (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C D) (P : Karoubi C) : (((functorExtension₂ C D).obj X).obj P).X = X.obj P.X

def CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] : (functorExtension₂ C D).comp ((Functor.whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)) ≅ (Functor.whiskeringRight C D (Karoubi D)).obj (toKaroubi D)

The natural isomorphism expressing that functors Karoubi C ⥤ Karoubi D obtained using functorExtension₂ actually extends the original functors C ⥤ D.

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C D) (X✝ : C) : (((functorExtension₂CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X✝).f = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (X : Functor C D) (X✝ : C) : (((functorExtension₂CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X✝).f = CategoryStruct.id (X.obj X✝)

noncomputable def CategoryTheory.Idempotents.karoubiUniversal₂ (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : Functor C D ≌ Functor (Karoubi C) (Karoubi D)

The equivalence of categories (C ⥤ D) ≌ (Karoubi C ⥤ Karoubi D) when D is idempotent complete.

theorem CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : (karoubiUniversal₂ C D).functor = functorExtension₂ C D

instance CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension₂ (C : Type u_1) (D : Type u_2) [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] [IsIdempotentComplete D] : (functorExtension₂ C D).IsEquivalence

noncomputable def CategoryTheory.Idempotents.functorExtension (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : Functor (Functor C D) (Functor (Karoubi C) D)

The extension of functors functor (C ⥤ D) ⥤ (Karoubi C ⥤ D) when D is idempotent complete.

@[simp]

theorem CategoryTheory.Idempotents.functorExtension_obj_obj (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] (X : Functor C D) (X✝ : Karoubi C) : ((functorExtension C D).obj X).obj X✝ = (toKaroubiEquivalence D).inverse.obj (((functorExtension₂ C D).obj X).obj X✝)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension_obj_map (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] (X : Functor C D) {X✝ Y✝ : Karoubi C} (f : X✝ ⟶ Y✝) : ((functorExtension C D).obj X).map f = (toKaroubiEquivalence D).inverse.map (((functorExtension₂ C D).obj X).map f)

@[simp]

theorem CategoryTheory.Idempotents.functorExtension_map_app (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] {X✝ Y✝ : Functor C D} (f : X✝ ⟶ Y✝) (X : Karoubi C) : ((functorExtension C D).map f).app X = (toKaroubiEquivalence D).inverse.map (((functorExtension₂ C D).map f).app X)

noncomputable def CategoryTheory.Idempotents.karoubiUniversal (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : Functor C D ≌ Functor (Karoubi C) D

The equivalence (C ⥤ D) ≌ (Karoubi C ⥤ D) when D is idempotent complete.

theorem CategoryTheory.Idempotents.karoubiUniversal_functor_eq (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : (karoubiUniversal C D).functor = functorExtension C D

instance CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension (C : Type u_1) (D : Type u_2) [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] [IsIdempotentComplete D] : (functorExtension C D).IsEquivalence

instance CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi (C : Type u_1) (D : Type u_2) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] : ((Functor.whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).IsEquivalence

theorem CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [IsIdempotentComplete D] {F G : Functor (Karoubi C) D} (τ : (toKaroubi C).comp F ⟶ (toKaroubi C).comp G) (P : Karoubi C) : (((Functor.whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app P = CategoryStruct.comp (F.map P.decompId_i) (CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p))