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 (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) :
CategoryStruct.comp P.p.f P.p.f = P.p.f
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) {Z : C} (h : P.X.X ⟶ Z) :
CategoryStruct.comp P.p.f (CategoryStruct.comp P.p.f h) = CategoryStruct.comp P.p.f h
source
theorem CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f (C : Type u_1) [Category.{u_2, u_1} C] {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) :
CategoryStruct.comp P.p.f f.f.f = CategoryStruct.comp f.f.f Q.p.f
source
theorem CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc (C : Type u_1) [Category.{u_2, u_1} C] {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) {Z : C} (h : Q.X.X ⟶ Z) :
CategoryStruct.comp P.p.f (CategoryStruct.comp f.f.f h) = CategoryStruct.comp f.f.f (CategoryStruct.comp Q.p.f h)
source
def CategoryTheory.Idempotents.KaroubiKaroubi.inverse (C : Type u_1) [Category.{u_2, u_1} C] :
Functor (Karoubi (Karoubi C)) (Karoubi C)

The canonical functor Karoubi (Karoubi C) ⥤ Karoubi C

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f (C : Type u_1) [Category.{u_2, u_1} C] {X✝ Y✝ : Karoubi (Karoubi C)} (f : X✝ ⟶ Y✝) :
      ((inverse C).map f).f = f.f.f
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) :
      ((inverse C).obj P).X = P.X.X
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) :
      ((inverse C).obj P).p = P.p.f
      source
      instance CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiInverse (C : Type u_1) [Category.{u_2, u_1} C] [Preadditive C] :
      (inverse C).Additive
      source
      def CategoryTheory.Idempotents.KaroubiKaroubi.unitIso (C : Type u_1) [Category.{u_2, u_1} C] :
      Functor.id (Karoubi C) ≅ (toKaroubi (Karoubi C)).comp (inverse C)

      The unit isomorphism of the equivalence

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

          The counit isomorphism of the equivalence

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) :
              ((counitIso C).hom.app P).f.f = P.p.f
              source
              @[simp]
              theorem CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f (C : Type u_1) [Category.{u_2, u_1} C] (P : Karoubi (Karoubi C)) :
              ((counitIso C).inv.app P).f.f = P.p.f
              source
              def CategoryTheory.Idempotents.KaroubiKaroubi.equivalence (C : Type u_1) [Category.{u_2, u_1} C] :
              Karoubi C ≌ Karoubi (Karoubi C)

              The equivalence Karoubi C ≌ Karoubi (Karoubi C)

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