# mathlib3documentation

category_theory.idempotents.functor_extension

# Extension of functors to the idempotent completion #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we construct an extension functor_extension₁ of functors C ⥤ karoubi D to functors karoubi C ⥤ karoubi D. This results in an equivalence karoubi_universal₁ C D : (C ⥤ karoubi D) ≌ (karoubi C ⥤ karoubi D).

We also construct an extension functor_extension₂ of functors (C ⥤ D) ⥤ (karoubi C ⥤ karoubi D). Moreover, when D is idempotent complete, we get equivalences karoubi_universal₂ C D : C ⥤ D ≌ karoubi C ⥤ karoubi D and karoubi_universal 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 category_theory.idempotents.nat_trans_eq {C : Type u_1} {D : Type u_2} {F G : D} (φ : F G)  :

A natural transformation between functors karoubi C ⥤ D is determined by its value on objects coming from C.

@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_map_f {C : Type u_1} {D : Type u_2} (F : C ) (f : P Q) :
= (F.map f.f).f

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

Equations
@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_obj_p {C : Type u_1} {D : Type u_2} (F : C )  :
= (F.map P.p).f
@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_obj_X {C : Type u_1} {D : Type u_2} (F : C )  :
= (F.obj P.X).X
@[simp]
theorem category_theory.idempotents.functor_extension₁.map_app_f {C : Type u_1} {D : Type u_2} {F G : C } (φ : F G)  :
= (F.map P.p).f (φ.app P.X).f
def category_theory.idempotents.functor_extension₁.map {C : Type u_1} {D : Type u_2} {F G : C } (φ : 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

Equations

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

Equations
@[simp]
theorem category_theory.idempotents.functor_extension₁_map (C : Type u_1) (D : Type u_2) (F G : C ) (φ : F G) :
@[simp]
@[simp]
@[simp]

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

Equations

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

Equations
@[simp]
@[simp]
@[simp]

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

Equations
@[simp]
theorem category_theory.idempotents.functor_extension₁_comp (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : C ) (G : D ) :
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_obj_p (C : Type u_1) (D : Type u_2) (X : C D)  :
.obj P).p = X.map P.p
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_map_f (C : Type u_1) (D : Type u_2) (X : C D) (f : P Q) :
.map f).f = X.map f.f
@[simp]
theorem category_theory.idempotents.functor_extension₂_map_app_f (C : Type u_1) (D : Type u_2) (_x _x_1 : C D) (f : _x _x_1)  :
.app P).f = f.app P.X _x_1.map P.p
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_obj_X (C : Type u_1) (D : Type u_2) (X : C D)  :
.obj P).X = X.obj P.X

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

Equations
Instances for category_theory.idempotents.functor_extension₂
@[simp]

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

Equations
@[simp]
@[protected, instance]
Equations
@[simp]
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_obj_X (C : Type u_1) (D : Type u_2) (X : C D)  :
P).X = X.obj P.X
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_map_app_f (C : Type u_1) (D : Type u_2) (_x _x_1 : C D) (f : _x _x_1)  :
P).f = f.app P.X _x_1.map P.p
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_obj_p (C : Type u_1) (D : Type u_2) (X : C D)  :
P).p = X.map P.p
@[simp]
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_obj_map (C : Type u_1) (D : Type u_2) (_x _x_1 : C) (f : _x _x_1) :
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_map_f (C : Type u_1) (D : Type u_2) (X : C D) (f : P Q) :
f).f = X.map f.f
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_counit_iso_inv_app_app_f (C : Type u_1) (D : Type u_2)  :
X_1).f = (X.map X_1.decomp_id_i).f (X.map X_1.p)).f 𝟙 (X.obj X_1.X)))
@[simp]
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_map_app (C : Type u_1) (D : Type u_2) (f : _x _x_1) (X : C) :
noncomputable def category_theory.idempotents.karoubi_universal₂ (C : Type u_1) (D : Type u_2)  :

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

Equations
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_obj_obj (C : Type u_1) (D : Type u_2) (X_1 : C) :
X_1 = (X.obj X_1))
@[protected, instance]
Equations
@[simp]
theorem category_theory.idempotents.functor_extension_obj_obj (C : Type u_1) (D : Type u_2) (X : C D)  :
noncomputable def category_theory.idempotents.functor_extension (C : Type u_1) (D : Type u_2)  :
(C D)

The extension of functors functor (C ⥤ D) ⥤ (karoubi C ⥤ D) when D is idempotent compltete.

Equations
Instances for category_theory.idempotents.functor_extension
@[simp]
theorem category_theory.idempotents.functor_extension_obj_map (C : Type u_1) (D : Type u_2) (X : C D) (_x _x_1 : category_theory.idempotents.karoubi C) (f : _x _x_1) :
@[simp]
theorem category_theory.idempotents.functor_extension_map_app (C : Type u_1) (D : Type u_2) (_x _x_1 : C D) (f : _x _x_1)  :
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_obj_map (C : Type u_1) (D : Type u_2) (X : C D) (_x _x_1 : category_theory.idempotents.karoubi C) (f : _x _x_1) :
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_map_app (C : Type u_1) (D : Type u_2) (_x _x_1 : D) (f : _x _x_1) (X : C) :
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_obj_map (C : Type u_1) (D : Type u_2) (_x _x_1 : C) (f : _x _x_1) :
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_obj_obj (C : Type u_1) (D : Type u_2) (X : C D)  :
X_1 =
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_map_app (C : Type u_1) (D : Type u_2) (_x _x_1 : C D) (f : _x _x_1)  :
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_obj_obj (C : Type u_1) (D : Type u_2) (X_1 : C) :
X_1 =
noncomputable def category_theory.idempotents.karoubi_universal (C : Type u_1) (D : Type u_2)  :

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations