Documentation

Mathlib.CategoryTheory.Idempotents.FunctorCategories

Idempotent completeness and functor categories #

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

We also provide a fully faithful functor karoubiFunctorCategoryEmbedding : 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.

Instances For

    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 toKaroubi C : C ⥤ Karoubi C.