mathlib documentation

category_theory.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 #

@[nolint]
structure category_theory.idempotents.karoubi (C : Type u_1) [category_theory.category C] :
Type (max u_1 u_2)
  • X : C
  • p : self.X self.X
  • idem : self.p self.p = self.p

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 enveloppe of C. It makes sense for any category C.

Instances for category_theory.idempotents.karoubi
theorem category_theory.idempotents.karoubi.hom.ext {C : Type u_1} {_inst_1 : category_theory.category C} {P Q : category_theory.idempotents.karoubi C} (x y : P.hom Q) (h : x.f = y.f) :
x = y
@[ext]

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 category_theory.idempotents.karoubi.hom
@[simp]
@[simp]
theorem category_theory.idempotents.karoubi.p_comp_assoc {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P.hom Q) {X' : C} (f' : Q.X X') :
P.p f.f f' = f.f f'
@[simp]
theorem category_theory.idempotents.karoubi.comp_p_assoc {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P.hom Q) {X' : C} (f' : Q.X X') :
f.f Q.p f' = f.f f'
theorem category_theory.idempotents.karoubi.comp_proof {C : Type u_1} [category_theory.category C] {P Q R : category_theory.idempotents.karoubi C} (g : Q.hom R) (f : P.hom Q) :
f.f g.f = P.p (f.f g.f) R.p
@[protected, instance]

The category structure on the karoubi envelope of a category.

Equations
@[simp]
theorem category_theory.idempotents.karoubi.comp {C : Type u_1} [category_theory.category C] {P Q R : category_theory.idempotents.karoubi C} (f : P Q) (g : Q R) :
f g = {f := f.f g.f, comm := _}
@[protected, instance]

It is possible to coerce an object of C into an object of karoubi C. See also the functor to_karoubi.

Equations
@[simp]
theorem category_theory.idempotents.karoubi.coe_X {C : Type u_1} [category_theory.category C] (X : C) :
X.X = X
@[simp]

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

Equations
Instances for category_theory.idempotents.to_karoubi
@[protected, instance]
Equations
  • category_theory.idempotents.quiver.hom.add_comm_group = {add := λ (f g : P Q), {f := f.f + g.f, comm := _}, add_assoc := _, zero := {f := 0, comm := _}, zero_add := _, add_zero := _, nsmul := add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7, nsmul_zero' := _, nsmul_succ' := _, neg := λ (f : P Q), {f := -f.f, comm := _}, sub := add_group.sub._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_11 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_12 category_theory.idempotents.quiver.hom.add_comm_group._proof_13 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_14 category_theory.idempotents.quiver.hom.add_comm_group._proof_15 (λ (f : P Q), {f := -f.f, comm := _}), sub_eq_add_neg := _, zsmul := add_group.zsmul._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_17 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_18 category_theory.idempotents.quiver.hom.add_comm_group._proof_19 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_20 category_theory.idempotents.quiver.hom.add_comm_group._proof_21 (λ (f : P Q), {f := -f.f, comm := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_sub {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (ᾰ ᾰ_1 : P Q) :
- ᾰ_1 = add_group.sub._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_11 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_12 category_theory.idempotents.quiver.hom.add_comm_group._proof_13 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_14 category_theory.idempotents.quiver.hom.add_comm_group._proof_15 (λ (f : P Q), {f := -f.f, comm := _}) ᾰ_1
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_zsmul {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (ᾰ : ) (ᾰ_1 : P Q) :
add_comm_group.zsmul ᾰ_1 = add_group.zsmul._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_17 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_18 category_theory.idempotents.quiver.hom.add_comm_group._proof_19 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_20 category_theory.idempotents.quiver.hom.add_comm_group._proof_21 (λ (f : P Q), {f := -f.f, comm := _}) ᾰ_1
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_nsmul {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (ᾰ : ) (ᾰ_1 : P Q) :
add_comm_group.nsmul ᾰ_1 = add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7 ᾰ_1

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

Equations
@[simp]
theorem category_theory.idempotents.karoubi.sum_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} {α : Type u_3} (s : finset α) (f : α → (P Q)) :
(s.sum (λ (x : α), f x)).f = s.sum (λ (x : α), (f x).f)

The split mono which appears in the factorisation decomp_id P.

Equations

The split epi which appears in the factorisation decomp_id P.

Equations

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.