Documentation

Mathlib.CategoryTheory.Idempotents.Karoubi

The Karoubi envelope of a category #

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

Main constructions and definitions #

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 : XX which is thought as the "formal image" of p. The type Karoubi C shall be the type of the objects of the karoubi envelope of C. It makes sense for any category C.

  • X : C

    an object of the underlying category

  • p : self.X self.X

    an endomorphism of the object

  • idem : CategoryTheory.CategoryStruct.comp self.p self.p = self.p

    the condition that the given endomorphism is an idempotent

Instances For
    @[simp]

    the condition that the given endomorphism is an idempotent

    theorem CategoryTheory.Idempotents.Karoubi.Hom.ext {C : Type u_1} :
    ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {P Q : CategoryTheory.Idempotents.Karoubi C} {x y : P.Hom Q}, x.f = y.fx = y

    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
      Equations
      • P.instInhabitedHomOfPreadditive Q = { default := { f := 0, comm := } }

      The category structure on the karoubi envelope of a category.

      Equations

      It is possible to coerce an object of C into an object of Karoubi C. See also the functor toKaroubi.

      Equations

      The obvious fully faithful functor toKaroubi sends an object X : C to the obvious formal direct factor of X given by 𝟙 X.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • CategoryTheory.Idempotents.instAdd = { add := fun (f g : P Q) => { f := f.f + g.f, comm := } }
        Equations
        • CategoryTheory.Idempotents.instNeg = { neg := fun (f : P Q) => { f := -f.f, comm := } }
        Equations
        • CategoryTheory.Idempotents.instZero = { zero := { f := 0, comm := } }

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

        Equations
        • P.inclusionHom Q = { toFun := fun (f : P Q) => f.f, map_zero' := , map_add' := }
        Instances For
          @[simp]
          theorem CategoryTheory.Idempotents.Karoubi.sum_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {P : CategoryTheory.Idempotents.Karoubi C} {Q : CategoryTheory.Idempotents.Karoubi C} {α : Type u_2} (s : Finset α) (f : α(P Q)) :
          (∑ xs, f x).f = xs, (f x).f

          The category Karoubi C is preadditive if C is.

          Equations

          If C is idempotent complete, the functor toKaroubi : C ⥤ Karoubi C is an equivalence.

          Equations
          • =

          The split mono which appears in the factorisation decompId P.

          Equations
          • P.decompId_i = { f := P.p, comm := }
          Instances For

            The split epi which appears in the factorisation decompId P.

            Equations
            • P.decompId_p = { f := P.p, comm := }
            Instances For

              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.