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.
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
Instances For
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 canonical functor (C ⥤ Karoubi D) ⥤ (Karoubi C ⥤ Karoubi D)
Instances For
The natural isomorphism expressing that functors Karoubi C ⥤ Karoubi D
obtained
using functorExtension₁
actually extends the original functors C ⥤ Karoubi D
.
Instances For
The counit isomorphism of the equivalence (C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)
.
Instances For
The equivalence of categories (C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)
.
Instances For
The canonical functor (C ⥤ D) ⥤ (Karoubi C ⥤ Karoubi D)
Instances For
The natural isomorphism expressing that functors Karoubi C ⥤ Karoubi D
obtained
using functorExtension₂
actually extends the original functors C ⥤ 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.