Documentation

Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

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.