Idempotent completeness and functor categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define an instance functor_category_is_idempotent_complete
expressing
that a functor category J ⥤ C
is idempotent complete when the target category C
is.
We also provide a fully faithful functor
karoubi_functor_category_embedding : karoubi (J ⥤ C)) : J ⥤ karoubi C
for all categories
J
and 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
.
Tautological action on maps of the functor karoubi (J ⥤ C) ⥤ (J ⥤ karoubi C)
.
Equations
- category_theory.idempotents.karoubi_functor_category_embedding.map f = {app := λ (j : J), {f := f.f.app j, comm := _}, naturality' := _}
The tautological fully faithful functor karoubi (J ⥤ C) ⥤ (J ⥤ karoubi C)
.
Equations
- category_theory.idempotents.karoubi_functor_category_embedding J C = {obj := category_theory.idempotents.karoubi_functor_category_embedding.obj _inst_2, map := λ (P Q : category_theory.idempotents.karoubi (J ⥤ C)), category_theory.idempotents.karoubi_functor_category_embedding.map, map_id' := _, map_comp' := _}
Instances for category_theory.idempotents.karoubi_functor_category_embedding
Equations
- category_theory.idempotents.karoubi_functor_category_embedding.category_theory.full J C = {preimage := λ (P Q : category_theory.idempotents.karoubi (J ⥤ C)) (f : (category_theory.idempotents.karoubi_functor_category_embedding J C).obj P ⟶ (category_theory.idempotents.karoubi_functor_category_embedding J C).obj Q), {f := {app := λ (j : J), (f.app j).f, naturality' := _}, comm := _}, witness' := _}
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
to_karoubi C : C ⥤ karoubi C
.