mathlib documentation

category_theory.idempotents.functor_extension

Extension of functors to the idempotent completion #

In this file, we construct an extension functor_extension₁ of functors C ⥤ karoubi D to functors karoubi C ⥤ karoubi D.

TODO : Obtain the equivalences karoubi_universal₁ C D : C ⥤ karoubi D ≌ karoubi C ⥤ karoubi D for all categories, and karoubi_universal C D : C ⥤ D ≌ karoubi C ⥤ D. when D is idempotent complete

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

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

Equations

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