mathlib documentation

category_theory.idempotents.functor_categories

Idempotent completeness and functor categories #

In this file we define an instance functor_category_is_idempotent_complete expressing that a functor category J ⥤ C is idempotent complete when the target category C is.

We also provide a fully faithful functor karoubi_functor_category_embedding : karoubi (J ⥤ C)) : J ⥤ karoubi C for all categories J and C.

On objects, the functor which sends a formal direct factor P of a functor F : J ⥤ C to the functor J ⥤ karoubi C which sends (j : J) to the corresponding direct factor of F.obj j.

Equations

The composition of (J ⥤ C) ⥤ karoubi (J ⥤ C) and karoubi (J ⥤ C) ⥤ (J ⥤ karoubi C) equals the functor (J ⥤ C) ⥤ (J ⥤ karoubi C) given by the composition with to_karoubi C : C ⥤ karoubi C.

@[simp]
theorem category_theory.idempotents.app_idem_assoc {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] (P : category_theory.idempotents.karoubi (J C)) (X : J) {X' : C} (f' : P.X.obj X X') :
P.p.app X P.p.app X f' = P.p.app X f'
@[simp]
theorem category_theory.idempotents.app_idem {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] (P : category_theory.idempotents.karoubi (J C)) (X : J) :
P.p.app X P.p.app X = P.p.app X
@[simp]
theorem category_theory.idempotents.app_p_comp_assoc {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) {X' : C} (f' : Q.X.obj X X') :
P.p.app X f.f.app X f' = f.f.app X f'
@[simp]
theorem category_theory.idempotents.app_p_comp {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) :
P.p.app X f.f.app X = f.f.app X
@[simp]
theorem category_theory.idempotents.app_comp_p_assoc {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) {X' : C} (f' : Q.X.obj X X') :
f.f.app X Q.p.app X f' = f.f.app X f'
@[simp]
theorem category_theory.idempotents.app_comp_p {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) :
f.f.app X Q.p.app X = f.f.app X
theorem category_theory.idempotents.app_p_comm {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) :
P.p.app X f.f.app X = f.f.app X Q.p.app X
theorem category_theory.idempotents.app_p_comm_assoc {J : Type u_1} {C : Type u_2} [category_theory.category J] [category_theory.category C] {P Q : category_theory.idempotents.karoubi (J C)} (f : P Q) (X : J) {X' : C} (f' : Q.X.obj X X') :
P.p.app X f.f.app X f' = f.f.app X Q.p.app X f'