mathlib documentation


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.


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.