mathlib3 documentation

category_theory.idempotents.karoubi_karoubi

Idempotence of the Karoubi envelope #

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

In this file, we construct the equivalence of categories karoubi_karoubi.equivalence C : karoubi C ≌ karoubi (karoubi C) for any category C.

source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.inverse_obj_X (C : Type u_1) [category_theory.category C] (P : category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)) :
((category_theory.idempotents.karoubi_karoubi.inverse C).obj P).X = P.X.X
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.inverse_map_f (C : Type u_1) [category_theory.category C] (P Q : category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)) (f : P ⟶ Q) :
((category_theory.idempotents.karoubi_karoubi.inverse C).map f).f = f.f.f
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.inverse_obj_p (C : Type u_1) [category_theory.category C] (P : category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)) :
((category_theory.idempotents.karoubi_karoubi.inverse C).obj P).p = P.p.f
source
def category_theory.idempotents.karoubi_karoubi.inverse (C : Type u_1) [category_theory.category C] :
category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C) ⥤ category_theory.idempotents.karoubi C

The canonical functor karoubi (karoubi C) ⥤ karoubi C

Equations
Instances for category_theory.idempotents.karoubi_karoubi.inverse
source
@[protected, instance]
def category_theory.idempotents.karoubi_karoubi.inverse.category_theory.functor.additive (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :
(category_theory.idempotents.karoubi_karoubi.inverse C).additive
source
def category_theory.idempotents.karoubi_karoubi.unit_iso (C : Type u_1) [category_theory.category C] :
𝟭 (category_theory.idempotents.karoubi C) ≅ category_theory.idempotents.to_karoubi (category_theory.idempotents.karoubi C) ⋙ category_theory.idempotents.karoubi_karoubi.inverse C

The unit isomorphism of the equivalence

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.unit_iso_hom (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.unit_iso C).hom = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.unit_iso_inv (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.unit_iso C).inv = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.counit_iso_hom_app_f_f (C : Type u_1) [category_theory.category C] (P : category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)) :
((category_theory.idempotents.karoubi_karoubi.counit_iso C).hom.app P).f.f = P.p.f
source
def category_theory.idempotents.karoubi_karoubi.counit_iso (C : Type u_1) [category_theory.category C] :
category_theory.idempotents.karoubi_karoubi.inverse C ⋙ category_theory.idempotents.to_karoubi (category_theory.idempotents.karoubi C) ≅ 𝟭 (category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C))

The counit isomorphism of the equivalence

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.counit_iso_inv_app_f_f (C : Type u_1) [category_theory.category C] (P : category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)) :
((category_theory.idempotents.karoubi_karoubi.counit_iso C).inv.app P).f.f = P.p.f
source
def category_theory.idempotents.karoubi_karoubi.equivalence (C : Type u_1) [category_theory.category C] :
category_theory.idempotents.karoubi C ≌ category_theory.idempotents.karoubi (category_theory.idempotents.karoubi C)

The equivalence karoubi C ≌ karoubi (karoubi C)

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.equivalence_inverse (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).inverse = category_theory.idempotents.karoubi_karoubi.inverse C
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.equivalence_counit_iso (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).counit_iso = category_theory.idempotents.karoubi_karoubi.counit_iso C
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.equivalence_functor (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).functor = category_theory.idempotents.to_karoubi (category_theory.idempotents.karoubi C)
source
@[simp]
theorem category_theory.idempotents.karoubi_karoubi.equivalence_unit_iso (C : Type u_1) [category_theory.category C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).unit_iso = category_theory.idempotents.karoubi_karoubi.unit_iso C
source
@[protected, instance]
def category_theory.idempotents.karoubi_karoubi.equivalence.additive_functor (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).functor.additive
source
@[protected, instance]
def category_theory.idempotents.karoubi_karoubi.equivalence.additive_inverse (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :
(category_theory.idempotents.karoubi_karoubi.equivalence C).inverse.additive