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 G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (φ : F ⟶ G) (P : CategoryTheory.Idempotents.Karoubi C) : φ.app P = CategoryTheory.CategoryStruct.comp (F.map P.decompId_i) (CategoryTheory.CategoryStruct.comp (φ.app { X := P.X, p := CategoryTheory.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} [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₁.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).obj P).p = (F.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).obj P).X = (F.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).map f).f = (F.map f.f).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 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₁.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 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.map P.p).f (φ.app P.X).f

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₁_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).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).map φ = CategoryTheory.Idempotents.FunctorExtension₁.map φ

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.Idempotents.functorExtension₁ C D).comp ((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).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.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.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.obj X✝).p

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.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi C)).comp (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_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.map P.decompId_i).f

@[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.map P.decompId_p).f

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.

@[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₁_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₁_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)).obj (CategoryTheory.Idempotents.toKaroubi C)

@[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

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).obj (F.comp ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)) ≅ ((CategoryTheory.Idempotents.functorExtension₁ C D).obj F).comp ((CategoryTheory.Idempotents.functorExtension₁ D E).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.

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₂_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✝ Y✝ : CategoryTheory.Idempotents.Karoubi C} (f : X✝ ⟶ Y✝) : (((CategoryTheory.Idempotents.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) [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).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) [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).map f).app P).f = CategoryTheory.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) [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).obj X).obj P).X = X.obj P.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.Idempotents.functorExtension₂ C D).comp ((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi C)) ≅ (CategoryTheory.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).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.

@[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.obj X✝)

@[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.obj X✝)

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

• CategoryTheory.Idempotents.karoubiUniversal₂ C D = (CategoryTheory.Idempotents.toKaroubi D).asEquivalence.congrRight.trans (CategoryTheory.Idempotents.karoubiUniversal₁ C D)

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

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

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.

@[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).obj X).obj X✝ = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.obj (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj X✝)

@[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✝ Y✝ : CategoryTheory.Idempotents.Karoubi C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Idempotents.functorExtension C D).obj X).map f = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f)

@[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 : CategoryTheory.Idempotents.Karoubi C) : ((CategoryTheory.Idempotents.functorExtension C D).map f).app X = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app X)

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

• CategoryTheory.Idempotents.karoubiUniversal C D = (CategoryTheory.Idempotents.karoubiUniversal₂ C D).trans (CategoryTheory.Idempotents.toKaroubi D).asEquivalence.symm.congrRight

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

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

instance CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi (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.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj (CategoryTheory.Idempotents.toKaroubi C)).IsEquivalence

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 G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (τ : (CategoryTheory.Idempotents.toKaroubi C).comp F ⟶ (CategoryTheory.Idempotents.toKaroubi C).comp G) (P : CategoryTheory.Idempotents.Karoubi C) : (((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj (CategoryTheory.Idempotents.toKaroubi C)).preimage τ).app P = CategoryTheory.CategoryStruct.comp (F.map P.decompId_i) (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p))