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

source
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

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

    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} [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
      source
      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)

      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) [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
        source
        @[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 φ
        source
        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 ((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.

        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) [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
          source
          @[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
          source
          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] :
          ((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).

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

            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) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] :
              (karoubiUniversal₁ C D).unitIso = (functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm
              source
              @[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
              source
              @[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 = (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)
              source
              @[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
              source
              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.

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

                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) [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
                  source
                  @[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
                  source
                  @[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)
                  source
                  @[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
                  source
                  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 ((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)) ≅ (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.

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

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

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

                        Equations
                        Instances For
                          source
                          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
                          source
                          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
                          source
                          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] :
                          ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).IsEquivalence
                          source
                          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) :
                          (((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))