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

theorem CategoryTheory.Idempotents.natTrans_eq {C : Type u_1} {D : Type u_2} [] [] (φ : F G) :

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} [] [] :
().p = (F.map P.p).f
@[simp]
theorem CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_X {C : Type u_1} {D : Type u_2} [] [] :
().X = (F.obj P.X).X
@[simp]
theorem CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f {C : Type u_1} {D : Type u_2} [] [] :
∀ {X Y : } (f : X Y), ().f = (F.map f.f).f

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

Instances For
@[simp]
theorem CategoryTheory.Idempotents.FunctorExtension₁.map_app_f {C : Type u_1} {D : Type u_2} [] [] (φ : F G) :
().f = CategoryTheory.CategoryStruct.comp (F.map P.p).f (φ.app P.X).f
def CategoryTheory.Idempotents.FunctorExtension₁.map {C : Type u_1} {D : Type u_2} [] [] (φ : F 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
@[simp]
@[simp]
theorem CategoryTheory.Idempotents.functorExtension₁_map (C : Type u_1) (D : Type u_2) [] [] :
∀ {X Y : } (φ : X Y),

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

Instances For

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

Instances For
@[simp]
theorem CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f (C : Type u_1) (D : Type u_2) [] [] :
((.app X).app P).f = ().f
@[simp]
theorem CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f (C : Type u_1) (D : Type u_2) [] [] :
((.app X).app P).f = ().f

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

Instances For
@[simp]
@[simp]
@[simp]

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

Instances For
theorem CategoryTheory.Idempotents.functorExtension₁_comp (C : Type u_1) (D : Type u_2) (E : Type u_3) [] [] [] :
().obj () = CategoryTheory.Functor.comp (().obj F) (().obj G)
@[simp]
theorem CategoryTheory.Idempotents.functorExtension₂_obj_obj_X (C : Type u_1) (D : Type u_2) [] [] (X : ) :
((().obj X).obj P).X = X.obj P.X
@[simp]
theorem CategoryTheory.Idempotents.functorExtension₂_obj_obj_p (C : Type u_1) (D : Type u_2) [] [] (X : ) :
((().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) [] [] :
∀ {X Y : } (f : X Y) (P : ), ((().map f).app P).f = CategoryTheory.CategoryStruct.comp (f.app P.X) (Y.map P.p)
@[simp]
theorem CategoryTheory.Idempotents.functorExtension₂_obj_map_f (C : Type u_1) (D : Type u_2) [] [] (X : ) :
∀ {X Y : } (f : X Y), ((().obj X).map f).f = X.map f.f

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

Instances For

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

Instances For
noncomputable def CategoryTheory.Idempotents.karoubiUniversal₂ (C : Type u_1) (D : Type u_2) [] [] :

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

Instances For
@[simp]
theorem CategoryTheory.Idempotents.functorExtension_map_app (C : Type u_1) (D : Type u_2) [] [] :
∀ {X Y : } (f : X Y) (X_1 : ), (().map f).app X_1 = ().map ((().map f).app X_1)
@[simp]
theorem CategoryTheory.Idempotents.functorExtension_obj_map (C : Type u_1) (D : Type u_2) [] [] (X : ) :
∀ {X Y : } (f : X Y), (().obj X).map f = ().map ((().obj X).map f)
@[simp]
theorem CategoryTheory.Idempotents.functorExtension_obj_obj (C : Type u_1) (D : Type u_2) [] [] (X : ) :
(().obj X).obj X = ().obj ((().obj X).obj X)
noncomputable def CategoryTheory.Idempotents.functorExtension (C : Type u_1) (D : Type u_2) [] [] :

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

Instances For
noncomputable def CategoryTheory.Idempotents.karoubiUniversal (C : Type u_1) (D : Type u_2) [] [] :

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

Instances For