Documentation

Mathlib.CategoryTheory.Idempotents.FunctorExtension

Extension of functors to the idempotent completion #

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

We also construct an extension functorExtension₂ of functors (C ⥤ D) ⥤ (Karoubi C ⥤ Karoubi D). Moreover, when D is idempotent complete, we get equivalences karoubiUniversal₂ C D : C ⥤ D ≌ Karoubi C ⥤ Karoubi D and karoubiUniversal 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.

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

Instances For

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

    Instances For

      The extension of functors functor (C ⥤ D) ⥤ (Karoubi C ⥤ D) when D is idempotent complete.

      Instances For

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

        Instances For