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} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {F : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} {G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (φ : F ⟶ G) (P : CategoryTheory.Idempotents.Karoubi C) : φ.app P = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.Idempotents.Karoubi.decompId_i P)) (CategoryTheory.CategoryStruct.comp (φ.app (CategoryTheory.Idempotents.Karoubi.mk P.X (CategoryTheory.CategoryStruct.id P.X))) (G.toPrefunctor.map (CategoryTheory.Idempotents.Karoubi.decompId_p P)))

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

def CategoryTheory.Idempotents.FunctorExtension₁.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} {G : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} (φ : F ⟶ G) : CategoryTheory.Idempotents.FunctorExtension₁.obj F ⟶ CategoryTheory.Idempotents.FunctorExtension₁.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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Idempotents.instIsEquivalenceKaroubiInstCategoryKaroubiToKaroubi (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.IsIdempotentComplete D] : CategoryTheory.IsEquivalence (CategoryTheory.Idempotents.toKaroubi D)

Equations

• CategoryTheory.Idempotents.instIsEquivalenceKaroubiInstCategoryKaroubiToKaroubi D = CategoryTheory.Idempotents.toKaroubiIsEquivalence D

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Idempotents.isEquivalence_whiskeringLeft_obj_toKaroubi_aux (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.IsIdempotentComplete D] : CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).toPrefunctor.obj (CategoryTheory.Idempotents.toKaroubi C)) (CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).toPrefunctor.obj (CategoryTheory.Idempotents.toKaroubi D)) ((CategoryTheory.whiskeringRight C (CategoryTheory.Idempotents.Karoubi D) D).toPrefunctor.obj (CategoryTheory.Functor.inv (CategoryTheory.Idempotents.toKaroubi D)))) = (CategoryTheory.Idempotents.karoubiUniversal C D).inverse

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

Equations

• One or more equations did not get rendered due to their size.

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