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.

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 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.

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

Equations
  • One or more equations did not get rendered due to their size.
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

    Equations
    • One or more equations did not get rendered due to their size.
    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)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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
        source
        @[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
        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.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.
        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 P.decompId_i).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 P.decompId_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.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.
          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₁CompWhiskeringLeftToKaroubiIso 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).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              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.
              Instances For
                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_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ Y), (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f).f = X.map f.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] (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₂_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_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
                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.
                Instances For
                  source
                  @[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)
                  source
                  @[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)
                  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.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.
                  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) (CategoryTheory.Idempotents.Karoubi D)

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

                    Equations
                    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.instIsEquivalenceFunctorKaroubiFunctorExtension₂ (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.functorExtension₂ C D).IsEquivalence
                      Equations
                      • ⋯ = ⋯
                      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_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ 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)
                      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.Idempotents.toKaroubiEquivalence D).inverse.obj (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X✝).obj X)
                      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.Idempotents.toKaroubiEquivalence D).inverse.map (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app X_1)
                      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.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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.

                        Equations
                        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.instIsEquivalenceFunctorKaroubiFunctorExtension (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.functorExtension C D).IsEquivalence
                          Equations
                          • ⋯ = ⋯
                          source
                          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
                          Equations
                          • ⋯ = ⋯
                          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.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))