Idempotent completeness and homological complexes #
This file contains simplifications lemmas for categories
Karoubi (HomologicalComplex C c)
and the construction of an equivalence
of categories Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c
.
When the category C
is idempotent complete, it is shown that
HomologicalComplex (Karoubi C) c
is also idempotent complete.
The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c
,
on objects.
Instances For
The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c
,
on morphisms.
Instances For
The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c
.
Instances For
The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)
,
on objects
Instances For
The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)
,
on morphisms
Instances For
The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)
.
Instances For
The counit isomorphism of the equivalence
Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c
.
Instances For
The unit isomorphism of the equivalence
Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c
.
Instances For
The equivalence Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c
.
Instances For
The equivalence Karoubi (ChainComplex C α) ≌ ChainComplex (Karoubi C) α
.
Instances For
The equivalence Karoubi (CochainComplex C α) ≌ CochainComplex (Karoubi C) α
.