Idempotence of the Karoubi envelope #
In this file, we construct the equivalence of categories
KaroubiKaroubi.equivalence C : Karoubi C ≌ Karoubi (Karoubi C)
for any category C
.
The canonical functor Karoubi (Karoubi C) ⥤ Karoubi C
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f
(C : Type u_1)
[Category.{u_2, u_1} C]
{X✝ Y✝ : Karoubi (Karoubi C)}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X
(C : Type u_1)
[Category.{u_2, u_1} C]
(P : Karoubi (Karoubi C))
:
@[simp]
theorem
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p
(C : Type u_1)
[Category.{u_2, u_1} C]
(P : Karoubi (Karoubi C))
:
instance
CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiInverse
(C : Type u_1)
[Category.{u_2, u_1} C]
[Preadditive C]
:
The unit isomorphism of the equivalence
Instances For
The counit isomorphism of the equivalence
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence Karoubi C ≌ Karoubi (Karoubi C)
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_functor
(C : Type u_1)
[Category.{u_2, u_1} C]
[Preadditive C]
:
instance
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse
(C : Type u_1)
[Category.{u_2, u_1} C]
[Preadditive C]
: