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.

@[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.toPrefunctor.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

@[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

@[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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.toPrefunctor.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

@[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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {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

@[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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.toPrefunctor.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

@[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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {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

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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C} (h : Q.X.toPrefunctor.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)

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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {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)

instance CategoryTheory.Idempotents.functor_category_isIdempotentComplete (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.IsIdempotentComplete C] : CategoryTheory.IsIdempotentComplete (CategoryTheory.Functor J C)

Equations

• (_ : CategoryTheory.IsIdempotentComplete (CategoryTheory.Functor J C)) = (_ : CategoryTheory.IsIdempotentComplete (CategoryTheory.Functor J C))

@[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).toPrefunctor.obj j).p = P.p.app j

@[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 ⟶ j') : ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).toPrefunctor.map φ).f = CategoryTheory.CategoryStruct.comp (P.p.app j) (P.X.toPrefunctor.map φ)

@[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).toPrefunctor.obj j).X = P.X.toPrefunctor.obj j

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.

@[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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {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

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 : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} {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

• CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f = CategoryTheory.NatTrans.mk fun (j : J) => CategoryTheory.Idempotents.Karoubi.Hom.mk (f.f.app j)

@[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).toPrefunctor.obj P = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P

@[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).toPrefunctor.map f = CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f

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.

instance CategoryTheory.Idempotents.instFullKaroubiFunctorCategoryInstCategoryKaroubiFunctorKaroubiInstCategoryKaroubiCategoryKaroubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] : CategoryTheory.Full (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Idempotents.instFaithfulKaroubiFunctorCategoryInstCategoryKaroubiFunctorKaroubiInstCategoryKaroubiCategoryKaroubiFunctorCategoryEmbedding (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] : CategoryTheory.Faithful (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C)) = (_ : CategoryTheory.Faithful (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C))

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.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Functor J C)) (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C) = (CategoryTheory.whiskeringRight J C (CategoryTheory.Idempotents.Karoubi C)).toPrefunctor.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.