Documentation

Mathlib.CategoryTheory.Idempotents.FunctorExtension

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.

We occasionally state and use equalities of functors because it is sometimes convenient to use rewrites when proving properties of functors obtained using the constructions in this file. Users are encouraged to use the corresponding natural isomorphism whenever possible.

source
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.map (CategoryTheory.Idempotents.Karoubi.decompId_i P)) (CategoryTheory.CategoryStruct.comp (φ.app (CategoryTheory.Idempotents.Karoubi.mk P.X (CategoryTheory.CategoryStruct.id P.X))) (G.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.

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

Instances For
    source
    @[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.map P.p).f (φ.app P.X).f
    source
    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

    Instances For
      source
      @[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
      source
      @[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 φ
      source
      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)

      Instances For
        source
        theorem CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi (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)).obj (CategoryTheory.Idempotents.toKaroubi C)) = CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
        source
        @[simp]
        theorem CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi_iso_inv (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₁_comp_whiskeringLeft_toKaroubi_iso C D).inv = CategoryTheory.eqToHom (_ : CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)) = CategoryTheory.Functor.comp (CategoryTheory.Idempotents.functorExtension₁ C D) ((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi C)))
        source
        @[simp]
        theorem CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi_iso_hom (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₁_comp_whiskeringLeft_toKaroubi_iso C D).hom = CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp (CategoryTheory.Idempotents.functorExtension₁ C D) ((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)))
        source
        def CategoryTheory.Idempotents.functorExtension₁_comp_whiskeringLeft_toKaroubi_iso (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)).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.

        Instances For
          source
          @[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 (CategoryTheory.Idempotents.Karoubi.decompId_i P)).f
          source
          @[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 (CategoryTheory.Idempotents.Karoubi.decompId_p P)).f
          source
          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)).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).

          Instances For
            source
            @[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₁_comp_whiskeringLeft_toKaroubi_iso C D).symm
            source
            @[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
            source
            @[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)
            source
            @[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
            source
            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).

            Instances For
              source
              theorem 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 (CategoryTheory.Functor.comp F ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)) = CategoryTheory.Functor.comp ((CategoryTheory.Idempotents.functorExtension₁ C D).obj F) ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)
              source
              @[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
              source
              @[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
              source
              @[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)
              source
              @[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
              source
              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)

              Instances For
                source
                theorem CategoryTheory.Idempotents.functorExtension₂_comp_whiskeringLeft_toKaroubi (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)).obj (CategoryTheory.Idempotents.toKaroubi C)) = (CategoryTheory.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi D)
                source
                @[simp]
                theorem CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_hom (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₂CompWhiskeringLeftToKaroubiIso C D).hom = CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp (CategoryTheory.Idempotents.functorExtension₂ C D) ((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))
                source
                @[simp]
                theorem CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_inv (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₂CompWhiskeringLeftToKaroubiIso C D).inv = CategoryTheory.eqToHom (_ : (CategoryTheory.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi D) = CategoryTheory.Functor.comp (CategoryTheory.Idempotents.functorExtension₂ C D) ((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi C)))
                source
                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)).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.

                Instances For
                  source
                  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)
                  source
                  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.

                  Instances For
                    source
                    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
                    source
                    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)
                    source
                    @[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).map f).app X_1 = (CategoryTheory.IsEquivalence.inverse (CategoryTheory.Idempotents.toKaroubi D)).map (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app X_1)
                    source
                    @[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.IsEquivalence.inverse (CategoryTheory.Idempotents.toKaroubi D)).map (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f)
                    source
                    @[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.IsEquivalence.inverse (CategoryTheory.Idempotents.toKaroubi D)).obj (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj X)
                    source
                    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.

                    Instances For
                      source
                      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.

                      Instances For
                        source
                        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
                        source
                        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)
                        source
                        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).obj (CategoryTheory.Idempotents.toKaroubi C)) (CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight C D (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi D)) ((CategoryTheory.whiskeringRight C (CategoryTheory.Idempotents.Karoubi D) D).obj (CategoryTheory.Functor.inv (CategoryTheory.Idempotents.toKaroubi D)))) = (CategoryTheory.Idempotents.karoubiUniversal C D).inverse
                        source
                        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).obj (CategoryTheory.Idempotents.toKaroubi C))
                        source
                        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).obj (CategoryTheory.Idempotents.toKaroubi C)).preimage τ).app P = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Idempotents.Karoubi.decompId_i P)) (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map (CategoryTheory.Idempotents.Karoubi.decompId_p P)))