mathlib3 documentation

category_theory.idempotents.karoubi

The Karoubi envelope of a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main constructions and definitions #

source
@[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
source
@[simp]
theorem category_theory.idempotents.karoubi.idem_assoc {C : Type u_1} [category_theory.category C] (self : category_theory.idempotents.karoubi C) {X' : C} (f' : self.X ⟶ X') :
self.p ≫ self.p ≫ f' = self.p ≫ f'
source
@[ext]
theorem category_theory.idempotents.karoubi.ext {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (h_X : P.X = Q.X) (h_p : P.p ≫ category_theory.eq_to_hom h_X = category_theory.eq_to_hom h_X ≫ Q.p) :
P = Q
source
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
source
theorem category_theory.idempotents.karoubi.hom.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} {P Q : category_theory.idempotents.karoubi C} (x y : P.hom Q) :
x = y ↔ x.f = y.f
source
@[ext]
structure category_theory.idempotents.karoubi.hom {C : Type u_1} [category_theory.category C] (P Q : category_theory.idempotents.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.

Instances for category_theory.idempotents.karoubi.hom
source
@[protected, instance]
def category_theory.idempotents.karoubi.hom.inhabited {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (P Q : category_theory.idempotents.karoubi C) :
inhabited (P.hom Q)
Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.hom_ext {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} {f g : P.hom Q} :
f = g ↔ f.f = g.f
source
@[simp]
theorem category_theory.idempotents.karoubi.p_comp {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P.hom Q) :
P.p ≫ f.f = f.f
source
@[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'
source
@[simp]
theorem category_theory.idempotents.karoubi.comp_p {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P.hom Q) :
f.f ≫ Q.p = f.f
source
@[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'
source
theorem category_theory.idempotents.karoubi.p_comm {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P.hom Q) :
P.p ≫ f.f = f.f ≫ Q.p
source
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
source
@[protected, instance]
def category_theory.idempotents.karoubi.category_theory.category {C : Type u_1} [category_theory.category C] :
category_theory.category (category_theory.idempotents.karoubi C)

The category structure on the karoubi envelope of a category.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.comp_f {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
source
@[simp]
theorem category_theory.idempotents.karoubi.id_eq {C : Type u_1} [category_theory.category C] {P : category_theory.idempotents.karoubi C} :
𝟙 P = {f := P.p, comm := _}
source
@[protected, instance]
def category_theory.idempotents.karoubi.coe {C : Type u_1} [category_theory.category C] :
has_coe_t C (category_theory.idempotents.karoubi C)

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

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.coe_X {C : Type u_1} [category_theory.category C] (X : C) :
↑X.X = X
source
@[simp]
theorem category_theory.idempotents.karoubi.coe_p {C : Type u_1} [category_theory.category C] (X : C) :
↑X.p = 𝟙 X
source
@[simp]
theorem category_theory.idempotents.karoubi.eq_to_hom_f {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (h : P = Q) :
(category_theory.eq_to_hom h).f = P.p ≫ category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.idempotents.to_karoubi_map_f (C : Type u_1) [category_theory.category C] (X Y : C) (f : X ⟶ Y) :
((category_theory.idempotents.to_karoubi C).map f).f = f
source
def category_theory.idempotents.to_karoubi (C : Type u_1) [category_theory.category C] :
C ⥤ category_theory.idempotents.karoubi C

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
source
@[simp]
theorem category_theory.idempotents.to_karoubi_obj_X (C : Type u_1) [category_theory.category C] (X : C) :
((category_theory.idempotents.to_karoubi C).obj X).X = X
source
@[simp]
theorem category_theory.idempotents.to_karoubi_obj_p (C : Type u_1) [category_theory.category C] (X : C) :
((category_theory.idempotents.to_karoubi C).obj X).p = 𝟙 X
source
@[protected, instance]
def category_theory.idempotents.to_karoubi.category_theory.full (C : Type u_1) [category_theory.category C] :
category_theory.full (category_theory.idempotents.to_karoubi C)
Equations
source
@[protected, instance]
def category_theory.idempotents.to_karoubi.category_theory.faithful (C : Type u_1) [category_theory.category C] :
category_theory.faithful (category_theory.idempotents.to_karoubi C)
source
@[protected, instance]
def category_theory.idempotents.quiver.hom.add_comm_group {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} :
add_comm_group (P ⟶ Q)
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 := _}
source
@[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
source
@[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
source
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_zero_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} :
0.f = 0
source
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_add_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (f g : P ⟶ Q) :
(f + g).f = f.f + g.f
source
@[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
source
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_neg_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (f : P ⟶ Q) :
(-f).f = -f.f
source
theorem category_theory.idempotents.karoubi.hom_eq_zero_iff {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} {f : P.hom Q} :
f = 0 ↔ f.f = 0
source
def category_theory.idempotents.karoubi.inclusion_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (P Q : category_theory.idempotents.karoubi C) :
(P ⟶ Q) →+ (P.X ⟶ Q.X)

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

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.inclusion_hom_apply {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (P Q : category_theory.idempotents.karoubi C) (f : P ⟶ Q) :
⇑(P.inclusion_hom Q) f = f.f
source
@[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)
source
@[protected, instance]
def category_theory.idempotents.karoubi.category_theory.preadditive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
category_theory.preadditive (category_theory.idempotents.karoubi C)

The category karoubi C is preadditive if C is.

Equations
source
@[protected, instance]
def category_theory.idempotents.to_karoubi.category_theory.functor.additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
(category_theory.idempotents.to_karoubi C).additive
source
@[protected, instance]
def category_theory.idempotents.karoubi.category_theory.is_idempotent_complete (C : Type u_1) [category_theory.category C] :
category_theory.is_idempotent_complete (category_theory.idempotents.karoubi C)
source
@[protected, instance]
def category_theory.idempotents.to_karoubi.category_theory.ess_surj (C : Type u_1) [category_theory.category C] [category_theory.is_idempotent_complete C] :
category_theory.ess_surj (category_theory.idempotents.to_karoubi C)
source
noncomputable def category_theory.idempotents.to_karoubi_is_equivalence (C : Type u_1) [category_theory.category C] [category_theory.is_idempotent_complete C] :
category_theory.is_equivalence (category_theory.idempotents.to_karoubi C)

If C is idempotent complete, the functor to_karoubi : C ⥤ karoubi C is an equivalence.

Equations
source
noncomputable def category_theory.idempotents.to_karoubi_equivalence (C : Type u_1) [category_theory.category C] [category_theory.is_idempotent_complete C] :
C ≌ category_theory.idempotents.karoubi C

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

Equations
source
@[protected, instance]
def category_theory.idempotents.to_karoubi_equivalence_functor_additive (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] [category_theory.is_idempotent_complete C] :
(category_theory.idempotents.to_karoubi_equivalence C).functor.additive
source
def category_theory.idempotents.karoubi.decomp_id_i {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
P ⟶ ↑(P.X)

The split mono which appears in the factorisation decomp_id P.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.decomp_id_i_f {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
P.decomp_id_i.f = P.p
source
def category_theory.idempotents.karoubi.decomp_id_p {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
↑(P.X) ⟶ P

The split epi which appears in the factorisation decomp_id P.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi.decomp_id_p_f {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
P.decomp_id_p.f = P.p
source
theorem category_theory.idempotents.karoubi.decomp_id {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
𝟙 P = P.decomp_id_i ≫ P.decomp_id_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.

source
theorem category_theory.idempotents.karoubi.decomp_p {C : Type u_1} [category_theory.category C] (P : category_theory.idempotents.karoubi C) :
(category_theory.idempotents.to_karoubi C).map P.p = P.decomp_id_p ≫ P.decomp_id_i
source
theorem category_theory.idempotents.karoubi.decomp_id_i_to_karoubi {C : Type u_1} [category_theory.category C] (X : C) :
((category_theory.idempotents.to_karoubi C).obj X).decomp_id_i = 𝟙 ((category_theory.idempotents.to_karoubi C).obj X)
source
theorem category_theory.idempotents.karoubi.decomp_id_p_to_karoubi {C : Type u_1} [category_theory.category C] (X : C) :
((category_theory.idempotents.to_karoubi C).obj X).decomp_id_p = 𝟙 ↑(((category_theory.idempotents.to_karoubi C).obj X).X)
source
theorem category_theory.idempotents.karoubi.decomp_id_i_naturality {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P ⟶ Q) :
f ≫ Q.decomp_id_i = P.decomp_id_i ≫ {f := f.f, comm := _}
source
theorem category_theory.idempotents.karoubi.decomp_id_p_naturality {C : Type u_1} [category_theory.category C] {P Q : category_theory.idempotents.karoubi C} (f : P ⟶ Q) :
P.decomp_id_p ≫ f = {f := f.f, comm := _} ≫ Q.decomp_id_p
source
@[simp]
theorem category_theory.idempotents.karoubi.zsmul_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {P Q : category_theory.idempotents.karoubi C} (n : ℤ) (f : P ⟶ Q) :
(n • f).f = n • f.f