Documentation

Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Idempotence of the Karoubi envelope #

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

source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) {Z : C} (h : P.X.X ⟶ Z) :
CategoryTheory.CategoryStruct.comp P.p.f (CategoryTheory.CategoryStruct.comp P.p.f h) = CategoryTheory.CategoryStruct.comp P.p.f h
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.idem_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) :
CategoryTheory.CategoryStruct.comp P.p.f P.p.f = P.p.f
source
theorem CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} {Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : P ⟶ Q) {Z : C} (h : Q.X.X ⟶ Z) :
CategoryTheory.CategoryStruct.comp P.p.f (CategoryTheory.CategoryStruct.comp f.f.f h) = CategoryTheory.CategoryStruct.comp f.f.f (CategoryTheory.CategoryStruct.comp Q.p.f h)
source
theorem CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} {Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : P ⟶ Q) :
CategoryTheory.CategoryStruct.comp P.p.f f.f.f = CategoryTheory.CategoryStruct.comp f.f.f Q.p.f
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
∀ {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : X ⟶ Y), ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).map f).f = f.f.f
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) :
((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).p = P.p.f
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) :
((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).X = P.X.X
source
def CategoryTheory.Idempotents.KaroubiKaroubi.inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) (CategoryTheory.Idempotents.Karoubi C)

The canonical functor Karoubi (Karoubi C) ⥤ Karoubi C

Instances For
    source
    instance CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiKaroubiInstCategoryKaroubiInstCategoryKaroubiInstPreadditiveKaroubiInstCategoryKaroubiInstPreadditiveKaroubiInstCategoryKaroubiInverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
    CategoryTheory.Functor.Additive (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C)
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_inv_app_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C) :
    ((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).inv.app X).f = X.p
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_hom_app_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C) :
    ((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).hom.app X).f = X.p
    source
    def CategoryTheory.Idempotents.KaroubiKaroubi.unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
    CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi C) ≅ CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)) (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C)

    The unit isomorphism of the equivalence

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) :
      ((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).inv.app P).f.f = P.p.f
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) :
      ((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).hom.app P).f.f = P.p.f
      source
      def CategoryTheory.Idempotents.KaroubiKaroubi.counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
      CategoryTheory.Functor.comp (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C) (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)) ≅ CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C))

      The counit isomorphism of the equivalence

      Instances For
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
        (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).counitIso = CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
        (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).functor = CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
        (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse = CategoryTheory.Idempotents.KaroubiKaroubi.inverse C
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
        (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).unitIso = CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C
        source
        def CategoryTheory.Idempotents.KaroubiKaroubi.equivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
        CategoryTheory.Idempotents.Karoubi C ≌ CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)

        The equivalence Karoubi C ≌ Karoubi (Karoubi C)

        Instances For
          source
          instance CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Functor.Additive (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).functor
          source
          instance CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Functor.Additive (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse