The Karoubi envelope of a category

In this file, we define the Karoubi envelope Karoubi C of a category C.

Main constructions and definitions

• Karoubi C is the Karoubi envelope of a category C: it is an idempotent complete category. It is also preadditive when C is preadditive.
• toKaroubi C : C ⥤ Karoubi C is a fully faithful functor, which is an equivalence (toKaroubiIsEquivalence) when C is idempotent complete.

structure CategoryTheory.Idempotents.Karoubi (C : Type u_1) [Category.{u_2, u_1} C] : Type (max u_1 u_2)

In a preadditive category C, when an object X decomposes as X ≅ P ⨿ Q, one may consider P as a direct factor of X and up to unique isomorphism, it is determined by the obvious idempotent X ⟶ P ⟶ X which is the projection onto P with kernel Q. More generally, one may define a formal direct factor of an object X : C : it consists of an idempotent p : X ⟶ X which is thought as the "formal image" of p. The type Karoubi C shall be the type of the objects of the karoubi envelope of C. It makes sense for any category C.

• X : C

  an object of the underlying category

• p : self.X ⟶ self.X

  an endomorphism of the object

• idem : CategoryStruct.comp self.p self.p = self.p

  the condition that the given endomorphism is an idempotent

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.idem_assoc {C : Type u_1} [Category.{u_2, u_1} C] (self : Karoubi C) {Z : C} (h : self.X ⟶ Z) : CategoryStruct.comp self.p (CategoryStruct.comp self.p h) = CategoryStruct.comp self.p h

theorem CategoryTheory.Idempotents.Karoubi.ext {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (h_X : P.X = Q.X) (h_p : CategoryStruct.comp P.p (eqToHom h_X) = CategoryStruct.comp (eqToHom h_X) Q.p) : P = Q

structure CategoryTheory.Idempotents.Karoubi.Hom {C : Type u_1} [Category.{u_2, u_1} C] (P Q : Karoubi C) : Type u_2

A morphism P ⟶ Q in the category Karoubi C is a morphism in the underlying category C which satisfies a relation, which in the preadditive case, expresses that it induces a map between the corresponding "formal direct factors" and that it vanishes on the complement formal direct factor.

• f : P.X ⟶ Q.X

  a morphism between the underlying objects

• comm : CategoryStruct.comp P.p (CategoryStruct.comp self.f Q.p) = self.f

  compatibility of the given morphism with the given idempotents

theorem CategoryTheory.Idempotents.Karoubi.Hom.ext_iff {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {P Q : Karoubi C} {x y : P.Hom Q} : x = y ↔ x.f = y.f

theorem CategoryTheory.Idempotents.Karoubi.Hom.ext {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {P Q : Karoubi C} {x y : P.Hom Q} (f : x.f = y.f) : x = y

instance CategoryTheory.Idempotents.Karoubi.instInhabitedHomOfPreadditive {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (P Q : Karoubi C) : Inhabited (P.Hom Q)

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.p_comp {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) : CategoryStruct.comp P.p f.f = f.f

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.p_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z) : CategoryStruct.comp P.p (CategoryStruct.comp f.f h) = CategoryStruct.comp f.f h

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.comp_p {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) : CategoryStruct.comp f.f Q.p = f.f

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.comp_p_assoc {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z) : CategoryStruct.comp f.f (CategoryStruct.comp Q.p h) = CategoryStruct.comp f.f h

theorem CategoryTheory.Idempotents.Karoubi.p_comm {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) : CategoryStruct.comp P.p f.f = CategoryStruct.comp f.f Q.p

theorem CategoryTheory.Idempotents.Karoubi.p_comm_assoc {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z) : CategoryStruct.comp P.p (CategoryStruct.comp f.f h) = CategoryStruct.comp f.f (CategoryStruct.comp Q.p h)

theorem CategoryTheory.Idempotents.Karoubi.comp_proof {C : Type u_1} [Category.{u_2, u_1} C] {P Q R : Karoubi C} (g : Q.Hom R) (f : P.Hom Q) : CategoryStruct.comp P.p (CategoryStruct.comp (CategoryStruct.comp f.f g.f) R.p) = CategoryStruct.comp f.f g.f

instance CategoryTheory.Idempotents.Karoubi.instCategory {C : Type u_1} [Category.{u_2, u_1} C] : Category.{u_2, max u_2 u_1} (Karoubi C)

The category structure on the karoubi envelope of a category.

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.hom_ext_iff {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f

theorem CategoryTheory.Idempotents.Karoubi.hom_ext {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.comp_f {C : Type u_1} [Category.{u_2, u_1} C] {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (CategoryStruct.comp f g).f = CategoryStruct.comp f.f g.f

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.id_f {C : Type u_1} [Category.{u_2, u_1} C] {P : Karoubi C} : (CategoryStruct.id P).f = P.p

instance CategoryTheory.Idempotents.Karoubi.coe {C : Type u_1} [Category.{u_2, u_1} C] : CoeTC C (Karoubi C)

It is possible to coerce an object of C into an object of Karoubi C. See also the functor toKaroubi.

theorem CategoryTheory.Idempotents.Karoubi.coe_X {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : { X := X, p := CategoryStruct.id X, idem := ⋯ }.X = X

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.coe_p {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : { X := X, p := CategoryStruct.id X, idem := ⋯ }.p = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.eqToHom_f {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (h : P = Q) : (eqToHom h).f = CategoryStruct.comp P.p (eqToHom ⋯)

def CategoryTheory.Idempotents.toKaroubi (C : Type u_1) [Category.{u_2, u_1} C] : Functor C (Karoubi C)

The obvious fully faithful functor toKaroubi sends an object X : C to the obvious formal direct factor of X given by 𝟙 X.

@[simp]

theorem CategoryTheory.Idempotents.toKaroubi_obj_X (C : Type u_1) [Category.{u_2, u_1} C] (X : C) : ((toKaroubi C).obj X).X = X

@[simp]

theorem CategoryTheory.Idempotents.toKaroubi_map_f (C : Type u_1) [Category.{u_2, u_1} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((toKaroubi C).map f).f = f

@[simp]

theorem CategoryTheory.Idempotents.toKaroubi_obj_p (C : Type u_1) [Category.{u_2, u_1} C] (X : C) : ((toKaroubi C).obj X).p = CategoryStruct.id X

instance CategoryTheory.Idempotents.instFullKaroubiToKaroubi (C : Type u_1) [Category.{u_2, u_1} C] : (toKaroubi C).Full

instance CategoryTheory.Idempotents.instFaithfulKaroubiToKaroubi (C : Type u_1) [Category.{u_2, u_1} C] : (toKaroubi C).Faithful

instance CategoryTheory.Idempotents.instAdd {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} : Add (P ⟶ Q)

@[simp]

theorem CategoryTheory.Idempotents.add_def {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} (f g : P ⟶ Q) : f + g = { f := f.f + g.f, comm := ⋯ }

instance CategoryTheory.Idempotents.instNeg {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} : Neg (P ⟶ Q)

@[simp]

theorem CategoryTheory.Idempotents.neg_def {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} (f : P ⟶ Q) : -f = { f := -f.f, comm := ⋯ }

instance CategoryTheory.Idempotents.instZero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} : Zero (P ⟶ Q)

@[simp]

theorem CategoryTheory.Idempotents.zero_def {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} : 0 = { f := 0, comm := ⋯ }

instance CategoryTheory.Idempotents.instAddCommGroupHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} : AddCommGroup (P ⟶ Q)

theorem CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} {f : P ⟶ Q} : f = 0 ↔ f.f = 0

def CategoryTheory.Idempotents.Karoubi.inclusionHom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (P Q : Karoubi C) : (P ⟶ Q) →+ (P.X ⟶ Q.X)

The map sending f : P ⟶ Q to f.f : P.X ⟶ Q.X is additive.

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.inclusionHom_apply {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] (P Q : Karoubi C) (f : P ⟶ Q) : (P.inclusionHom Q) f = f.f

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.sum_hom {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {P Q : Karoubi C} {α : Type u_2} (s : Finset α) (f : α → (P ⟶ Q)) : (∑ x ∈ s, f x).f = ∑ x ∈ s, (f x).f

instance CategoryTheory.Idempotents.instPreadditiveKaroubi {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] : Preadditive (Karoubi C)

The category Karoubi C is preadditive if C is.

instance CategoryTheory.Idempotents.instAdditiveKaroubiToKaroubi {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] : (toKaroubi C).Additive

instance CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi (C : Type u_1) [Category.{u_2, u_1} C] : IsIdempotentComplete (Karoubi C)

instance CategoryTheory.Idempotents.instEssSurjKaroubiToKaroubiOfIsIdempotentComplete (C : Type u_1) [Category.{u_2, u_1} C] [IsIdempotentComplete C] : (toKaroubi C).EssSurj

instance CategoryTheory.Idempotents.toKaroubi_isEquivalence (C : Type u_1) [Category.{u_2, u_1} C] [IsIdempotentComplete C] : (toKaroubi C).IsEquivalence

If C is idempotent complete, the functor toKaroubi : C ⥤ Karoubi C is an equivalence.

def CategoryTheory.Idempotents.toKaroubiEquivalence (C : Type u_1) [Category.{u_2, u_1} C] [IsIdempotentComplete C] : C ≌ Karoubi C

The equivalence C ≅ Karoubi C when C is idempotent complete.

instance CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] : (toKaroubiEquivalence C).functor.Additive

def CategoryTheory.Idempotents.Karoubi.decompId_i {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : P ⟶ { X := P.X, p := CategoryStruct.id P.X, idem := ⋯ }

The split mono which appears in the factorisation decompId P.

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.decompId_i_f {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : P.decompId_i.f = P.p

def CategoryTheory.Idempotents.Karoubi.decompId_p {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : { X := P.X, p := CategoryStruct.id P.X, idem := ⋯ } ⟶ P

The split epi which appears in the factorisation decompId P.

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.decompId_p_f {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : P.decompId_p.f = P.p

theorem CategoryTheory.Idempotents.Karoubi.decompId {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : CategoryStruct.id P = CategoryStruct.comp P.decompId_i P.decompId_p

The formal direct factor of P.X given by the idempotent P.p in the category C is actually a direct factor in the category Karoubi C.

theorem CategoryTheory.Idempotents.Karoubi.decompId_assoc {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) {Z : Karoubi C} (h : P ⟶ Z) : h = CategoryStruct.comp P.decompId_i (CategoryStruct.comp P.decompId_p h)

theorem CategoryTheory.Idempotents.Karoubi.decomp_p {C : Type u_1} [Category.{u_2, u_1} C] (P : Karoubi C) : (toKaroubi C).map P.p = CategoryStruct.comp P.decompId_p P.decompId_i

theorem CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : ((toKaroubi C).obj X).decompId_i = CategoryStruct.id ((toKaroubi C).obj X)

theorem CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : ((toKaroubi C).obj X).decompId_p = CategoryStruct.id { X := ((toKaroubi C).obj X).X, p := CategoryStruct.id ((toKaroubi C).obj X).X, idem := ⋯ }

theorem CategoryTheory.Idempotents.Karoubi.decompId_i_naturality {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P ⟶ Q) : CategoryStruct.comp f Q.decompId_i = CategoryStruct.comp P.decompId_i { f := f.f, comm := ⋯ }

theorem CategoryTheory.Idempotents.Karoubi.decompId_p_naturality {C : Type u_1} [Category.{u_2, u_1} C] {P Q : Karoubi C} (f : P ⟶ Q) : CategoryStruct.comp P.decompId_p f = CategoryStruct.comp { f := f.f, comm := ⋯ } Q.decompId_p

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.zsmul_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {P Q : Karoubi C} (n : ℤ) (f : P ⟶ Q) : (n • f).f = n • f.f