Documentation

Mathlib.CategoryTheory.Idempotents.FunctorCategories

Idempotent completeness and functor categories #

In this file we define an instance functor_category_isIdempotentComplete expressing that a functor category J ⥤ C is idempotent complete when the target category C is.

We also provide a fully faithful functor karoubiFunctorCategoryEmbedding : Karoubi (J ⥤ C)) : J ⥤ Karoubi C for all categories J and C.

source
@[simp]
theorem CategoryTheory.Idempotents.app_idem {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) (X : J) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (P.p.app X) = P.p.app X
source
@[simp]
theorem CategoryTheory.Idempotents.app_idem_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) (X : J) {Z : C} (h : P.X.obj X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (P.p.app X) h) = CategoryTheory.CategoryStruct.comp (P.p.app X) h
source
@[simp]
theorem CategoryTheory.Idempotents.app_p_comp {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (f.f.app X) = f.f.app X
source
@[simp]
theorem CategoryTheory.Idempotents.app_p_comp_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.obj X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (f.f.app X) h) = CategoryTheory.CategoryStruct.comp (f.f.app X) h
source
@[simp]
theorem CategoryTheory.Idempotents.app_comp_p {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) :
CategoryTheory.CategoryStruct.comp (f.f.app X) (Q.p.app X) = f.f.app X
source
@[simp]
theorem CategoryTheory.Idempotents.app_comp_p_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.obj X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (f.f.app X) (CategoryTheory.CategoryStruct.comp (Q.p.app X) h) = CategoryTheory.CategoryStruct.comp (f.f.app X) h
source
theorem CategoryTheory.Idempotents.app_p_comm {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (f.f.app X) = CategoryTheory.CategoryStruct.comp (f.f.app X) (Q.p.app X)
source
theorem CategoryTheory.Idempotents.app_p_comm_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.obj X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (f.f.app X) h) = CategoryTheory.CategoryStruct.comp (f.f.app X) (CategoryTheory.CategoryStruct.comp (Q.p.app X) h)
source
instance CategoryTheory.Idempotents.functor_category_isIdempotentComplete (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.IsIdempotentComplete C] :
CategoryTheory.IsIdempotentComplete (CategoryTheory.Functor J C)
Equations
  • ⋯ = ⋯
source
def CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) :
CategoryTheory.Functor J (CategoryTheory.Idempotents.Karoubi C)

On objects, the functor which sends a formal direct factor P of a functor F : J ⥤ C to the functor J ⥤ Karoubi C which sends (j : J) to the corresponding direct factor of F.obj j.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) (j : J) :
    ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).p = P.p.app j
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_X {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) (j : J) :
    ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).X = P.X.obj j
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) {j j' : J} (φ : j ⟶ j') :
    ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).map φ).f = CategoryTheory.CategoryStruct.comp (P.p.app j) (P.X.map φ)
    source
    def CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) :
    CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P ⟶ CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj Q

    Tautological action on maps of the functor Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C).

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (j : J) :
      ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f).app j).f = f.f.app j
      source
      def CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] :
      CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) (CategoryTheory.Functor J (CategoryTheory.Idempotents.Karoubi C))

      The tautological fully faithful functor Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_map (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] {X✝ Y✝ : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : X✝ ⟶ Y✝) :
        (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).map f = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f
        source
        @[simp]
        theorem CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_obj (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)) :
        (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).obj P = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P
        source
        instance CategoryTheory.Idempotents.instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] :
        (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).Full
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.Idempotents.instFaithfulKaroubiFunctorKaroubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_3, u_2} C] :
        (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).Faithful
        Equations
        • ⋯ = ⋯
        source
        theorem CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] :
        (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Functor J C)).comp (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C) = (CategoryTheory.whiskeringRight J C (CategoryTheory.Idempotents.Karoubi C)).obj (CategoryTheory.Idempotents.toKaroubi C)

        The composition of (J ⥤ C) ⥤ Karoubi (J ⥤ C) and Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C) equals the functor (J ⥤ C) ⥤ (J ⥤ Karoubi C) given by the composition with toKaroubi C : C ⥤ Karoubi C.