Documentation

Mathlib.CategoryTheory.Idempotents.Karoubi

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) [CategoryTheory.Category.{u_2, u_1} C] :

Type (max u_1 u_2)

X : C
an object of the underlying category
p : s.X ⟶ s.X
an endomorphism of the object
idem : CategoryTheory.CategoryStruct.comp s.p s.p = s.p
the condition that the given endomorphism is an idempotent

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.

Instances For

@[simp]

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

CategoryTheory.CategoryStruct.comp self.p (CategoryTheory.CategoryStruct.comp self.p h) = CategoryTheory.CategoryStruct.comp self.p h

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

P = Q

theorem CategoryTheory.Idempotents.Karoubi.Hom.ext {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C} (x y : CategoryTheory.Idempotents.Karoubi.Hom P Q), x.f = y.f → x = y

theorem CategoryTheory.Idempotents.Karoubi.Hom.ext_iff {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C} (x y : CategoryTheory.Idempotents.Karoubi.Hom P Q), x = y ↔ x.f = y.f

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

Type u_2

f : P.X ⟶ Q.X
a morphism between the underlying objects
comm : s.f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp s.f Q.p)
compatibility of the given morphism with the given idempotents

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.

Instances For

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

Inhabited (CategoryTheory.Idempotents.Karoubi.Hom P Q)

@[simp]

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

CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f.f h) = CategoryTheory.CategoryStruct.comp f.f h

@[simp]

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

CategoryTheory.CategoryStruct.comp P.p f.f = f.f

@[simp]

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

CategoryTheory.CategoryStruct.comp f.f (CategoryTheory.CategoryStruct.comp Q.p h) = CategoryTheory.CategoryStruct.comp f.f h

@[simp]

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

CategoryTheory.CategoryStruct.comp f.f Q.p = f.f

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

CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f.f h) = CategoryTheory.CategoryStruct.comp f.f (CategoryTheory.CategoryStruct.comp Q.p h)

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

CategoryTheory.CategoryStruct.comp P.p f.f = CategoryTheory.CategoryStruct.comp f.f Q.p

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

CategoryTheory.CategoryStruct.comp f.f g.f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f.f g.f) R.p)

instance CategoryTheory.Idempotents.Karoubi.instCategoryKaroubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :

CategoryTheory.Category.{u_2, max u_2 u_1} (CategoryTheory.Idempotents.Karoubi C)

The category structure on the karoubi envelope of a category.

@[simp]

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

f = g ↔ f.f = g.f

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

f = g

@[simp]

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

(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.id_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {P : CategoryTheory.Idempotents.Karoubi C} :

CategoryTheory.CategoryStruct.id P = CategoryTheory.Idempotents.Karoubi.Hom.mk P.p

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

CoeTC C (CategoryTheory.Idempotents.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} [CategoryTheory.Category.{u_2, u_1} C] (X : C) :

(CategoryTheory.Idempotents.Karoubi.mk X (CategoryTheory.CategoryStruct.id X)).X = X

@[simp]

theorem CategoryTheory.Idempotents.Karoubi.coe_p {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) :

(CategoryTheory.Idempotents.Karoubi.mk X (CategoryTheory.CategoryStruct.id X)).p = CategoryTheory.CategoryStruct.id X

@[simp]

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

(CategoryTheory.eqToHom h).f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.eqToHom (_ : P.X = Q.X))

@[simp]

theorem CategoryTheory.Idempotents.toKaroubi_obj_p (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : C) :

((CategoryTheory.Idempotents.toKaroubi C).obj X).p = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Idempotents.toKaroubi_map_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :

∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Idempotents.toKaroubi C).map f).f = f

@[simp]

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

((CategoryTheory.Idempotents.toKaroubi C).obj X).X = X

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

CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi C)

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

Instances For

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

CategoryTheory.Full (CategoryTheory.Idempotents.toKaroubi C)

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

CategoryTheory.Faithful (CategoryTheory.Idempotents.toKaroubi C)

@[simp]

theorem CategoryTheory.Idempotents.instAddCommGroupHom_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {P : CategoryTheory.Idempotents.Karoubi C} {Q : CategoryTheory.Idempotents.Karoubi C} :

0 = CategoryTheory.Idempotents.Karoubi.Hom.mk 0

@[simp]

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

-f = CategoryTheory.Idempotents.Karoubi.Hom.mk (-f.f)

@[simp]

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

f + g = CategoryTheory.Idempotents.Karoubi.Hom.mk (f.f + g.f)

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

AddCommGroup (P ⟶ Q)

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

f = 0 ↔ f.f = 0

@[simp]

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

↑(CategoryTheory.Idempotents.Karoubi.inclusionHom P Q) f = f.f

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

(P ⟶ Q) →+ (P.X ⟶ Q.X)

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

Instances For

@[simp]

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

(Finset.sum s fun x => f x).f = Finset.sum s fun x => (f x).f

instance CategoryTheory.Idempotents.instPreadditiveKaroubiInstCategoryKaroubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :

CategoryTheory.Preadditive (CategoryTheory.Idempotents.Karoubi C)

The category Karoubi C is preadditive if C is.

instance CategoryTheory.Idempotents.instAdditiveKaroubiInstCategoryKaroubiInstPreadditiveKaroubiInstCategoryKaroubiToKaroubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :

CategoryTheory.Functor.Additive (CategoryTheory.Idempotents.toKaroubi C)

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

CategoryTheory.IsIdempotentComplete (CategoryTheory.Idempotents.Karoubi C)

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

CategoryTheory.EssSurj (CategoryTheory.Idempotents.toKaroubi C)

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

CategoryTheory.IsEquivalence (CategoryTheory.Idempotents.toKaroubi C)

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

Instances For

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

C ≌ CategoryTheory.Idempotents.Karoubi C

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

Instances For

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

CategoryTheory.Functor.Additive (CategoryTheory.Idempotents.toKaroubiEquivalence C).functor

@[simp]

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

(CategoryTheory.Idempotents.Karoubi.decompId_i P).f = P.p

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

P ⟶ CategoryTheory.Idempotents.Karoubi.mk P.X (CategoryTheory.CategoryStruct.id P.X)

The split mono which appears in the factorisation decompId P.

Instances For

@[simp]

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

(CategoryTheory.Idempotents.Karoubi.decompId_p P).f = P.p

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

CategoryTheory.Idempotents.Karoubi.mk P.X (CategoryTheory.CategoryStruct.id P.X) ⟶ P

The split epi which appears in the factorisation decompId P.

Instances For

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

h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_i P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_p P) h)

theorem CategoryTheory.Idempotents.Karoubi.decompId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C) :

CategoryTheory.CategoryStruct.id P = CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_i P) (CategoryTheory.Idempotents.Karoubi.decompId_p 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.decomp_p {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C) :

(CategoryTheory.Idempotents.toKaroubi C).map P.p = CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_p P) (CategoryTheory.Idempotents.Karoubi.decompId_i P)

theorem CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) :

CategoryTheory.Idempotents.Karoubi.decompId_i ((CategoryTheory.Idempotents.toKaroubi C).obj X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X)

theorem CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) :

CategoryTheory.Idempotents.Karoubi.decompId_p ((CategoryTheory.Idempotents.toKaroubi C).obj X) = CategoryTheory.CategoryStruct.id (CategoryTheory.Idempotents.Karoubi.mk ((CategoryTheory.Idempotents.toKaroubi C).obj X).X (CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X).X))

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

CategoryTheory.CategoryStruct.comp f (CategoryTheory.Idempotents.Karoubi.decompId_i Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_i P) (CategoryTheory.Idempotents.Karoubi.Hom.mk f.f)

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.decompId_p P) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Idempotents.Karoubi.Hom.mk f.f) (CategoryTheory.Idempotents.Karoubi.decompId_p Q)

@[simp]

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

(n • f).f = n • f.f