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
  • One or more equations did not get rendered due to their size.
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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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