mathlib3 documentation

category_theory.idempotents.functor_extension

Extension of functors to the idempotent completion #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we construct an extension functor_extension₁ of functors C ⥤ karoubi D to functors karoubi C ⥤ karoubi D. This results in an equivalence karoubi_universal₁ C D : (C ⥤ karoubi D) ≌ (karoubi C ⥤ karoubi D).

We also construct an extension functor_extension₂ of functors (C ⥤ D) ⥤ (karoubi C ⥤ karoubi D). Moreover, when D is idempotent complete, we get equivalences karoubi_universal₂ C D : C ⥤ D ≌ karoubi C ⥤ karoubi D and karoubi_universal C D : C ⥤ D ≌ karoubi C ⥤ D.

We occasionally state and use equalities of functors because it is sometimes convenient to use rewrites when proving properties of functors obtained using the constructions in this file. Users are encouraged to use the corresponding natural isomorphism whenever possible.

source
theorem category_theory.idempotents.nat_trans_eq {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {F G : category_theory.idempotents.karoubi C ⥤ D} (φ : F ⟶ G) (P : category_theory.idempotents.karoubi C) :
φ.app P = F.map P.decomp_id_i ≫ φ.app ↑(P.X) ≫ G.map P.decomp_id_p

A natural transformation between functors karoubi C ⥤ D is determined by its value on objects coming from C.

source
@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_map_f {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (F : C ⥤ category_theory.idempotents.karoubi D) (P Q : category_theory.idempotents.karoubi C) (f : P ⟶ Q) :
((category_theory.idempotents.functor_extension₁.obj F).map f).f = (F.map f.f).f
source
def category_theory.idempotents.functor_extension₁.obj {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (F : C ⥤ category_theory.idempotents.karoubi D) :
category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D

The canonical extension of a functor C ⥤ karoubi D to a functor karoubi C ⥤ karoubi D

Equations
source
@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_obj_p {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (F : C ⥤ category_theory.idempotents.karoubi D) (P : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.functor_extension₁.obj F).obj P).p = (F.map P.p).f
source
@[simp]
theorem category_theory.idempotents.functor_extension₁.obj_obj_X {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (F : C ⥤ category_theory.idempotents.karoubi D) (P : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.functor_extension₁.obj F).obj P).X = (F.obj P.X).X
source
@[simp]
theorem category_theory.idempotents.functor_extension₁.map_app_f {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {F G : C ⥤ category_theory.idempotents.karoubi D} (φ : F ⟶ G) (P : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.functor_extension₁.map φ).app P).f = (F.map P.p).f ≫ (φ.app P.X).f
source
def category_theory.idempotents.functor_extension₁.map {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {F G : C ⥤ category_theory.idempotents.karoubi D} (φ : F ⟶ G) :
category_theory.idempotents.functor_extension₁.obj F ⟶ category_theory.idempotents.functor_extension₁.obj G

Extension of a natural transformation φ between functors C ⥤ karoubi D to a natural transformation between the extension of these functors to karoubi C ⥤ karoubi D

Equations
source
def category_theory.idempotents.functor_extension₁ (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(C ⥤ category_theory.idempotents.karoubi D) ⥤ category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D

The canonical functor (C ⥤ karoubi D) ⥤ (karoubi C ⥤ karoubi D)

Equations
source
@[simp]
theorem category_theory.idempotents.functor_extension₁_map (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (F G : C ⥤ category_theory.idempotents.karoubi D) (φ : F ⟶ G) :
(category_theory.idempotents.functor_extension₁ C D).map φ = category_theory.idempotents.functor_extension₁.map φ
source
@[simp]
theorem category_theory.idempotents.functor_extension₁_obj (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (F : C ⥤ category_theory.idempotents.karoubi D) :
(category_theory.idempotents.functor_extension₁ C D).obj F = category_theory.idempotents.functor_extension₁.obj F
source
theorem category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
category_theory.idempotents.functor_extension₁ C D ⋙ (category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C) = 𝟭 (C ⥤ category_theory.idempotents.karoubi D)
source
@[simp]
theorem category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso_hom (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso C D).hom = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso_inv (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso C D).inv = category_theory.eq_to_hom _
source
def category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
category_theory.idempotents.functor_extension₁ C D ⋙ (category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C) ≅ 𝟭 (C ⥤ category_theory.idempotents.karoubi D)

The natural isomorphism expressing that functors karoubi C ⥤ karoubi D obtained using functor_extension₁ actually extends the original functors C ⥤ karoubi D.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁.counit_iso_hom_app_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₁.counit_iso C D).hom.app X).app P).f = (X.map P.decomp_id_p).f
source
def category_theory.idempotents.karoubi_universal₁.counit_iso (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C) ⋙ category_theory.idempotents.functor_extension₁ C D ≅ 𝟭 (category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D)

The counit isomorphism of the equivalence (C ⥤ karoubi D) ≌ (karoubi C ⥤ karoubi D).

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁.counit_iso_inv_app_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₁.counit_iso C D).inv.app X).app P).f = (X.map P.decomp_id_i).f
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁_inverse (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.karoubi_universal₁ C D).inverse = (category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁_functor (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.karoubi_universal₁ C D).functor = category_theory.idempotents.functor_extension₁ C D
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁_unit_iso (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.karoubi_universal₁ C D).unit_iso = (category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso C D).symm
source
def category_theory.idempotents.karoubi_universal₁ (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
C ⥤ category_theory.idempotents.karoubi D ≌ category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D

The equivalence of categories (C ⥤ karoubi D) ≌ (karoubi C ⥤ karoubi D).

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₁_counit_iso (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.karoubi_universal₁ C D).counit_iso = category_theory.idempotents.karoubi_universal₁.counit_iso C D
source
theorem category_theory.idempotents.functor_extension₁_comp (C : Type u_1) (D : Type u_2) (E : Type u_3) [category_theory.category C] [category_theory.category D] [category_theory.category E] (F : C ⥤ category_theory.idempotents.karoubi D) (G : D ⥤ category_theory.idempotents.karoubi E) :
(category_theory.idempotents.functor_extension₁ C E).obj (F ⋙ (category_theory.idempotents.functor_extension₁ D E).obj G) = (category_theory.idempotents.functor_extension₁ C D).obj F ⋙ (category_theory.idempotents.functor_extension₁ D E).obj G
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_obj_p (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (X : C ⥤ D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.functor_extension₂ C D).obj X).obj P).p = X.map P.p
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_map_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (X : C ⥤ D) (P Q : category_theory.idempotents.karoubi C) (f : P ⟶ Q) :
(((category_theory.idempotents.functor_extension₂ C D).obj X).map f).f = X.map f.f
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_map_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (_x _x_1 : C ⥤ D) (f : _x ⟶ _x_1) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.functor_extension₂ C D).map f).app P).f = f.app P.X ≫ _x_1.map P.p
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_obj_obj_X (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] (X : C ⥤ D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.functor_extension₂ C D).obj X).obj P).X = X.obj P.X
source
def category_theory.idempotents.functor_extension₂ (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(C ⥤ D) ⥤ category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D

The canonical functor (C ⥤ D) ⥤ (karoubi C ⥤ karoubi D)

Equations
Instances for category_theory.idempotents.functor_extension₂
source
theorem category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
category_theory.idempotents.functor_extension₂ C D ⋙ (category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C) = (category_theory.whiskering_right C D (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi D)
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso_inv (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso C D).inv = category_theory.eq_to_hom _
source
def category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
category_theory.idempotents.functor_extension₂ C D ⋙ (category_theory.whiskering_left C (category_theory.idempotents.karoubi C) (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi C) ≅ (category_theory.whiskering_right C D (category_theory.idempotents.karoubi D)).obj (category_theory.idempotents.to_karoubi D)

The natural isomorphism expressing that functors karoubi C ⥤ karoubi D obtained using functor_extension₂ actually extends the original functors C ⥤ D.

Equations
source
@[simp]
theorem category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso_hom (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] :
(category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso C D).hom = category_theory.eq_to_hom _
source
@[protected, instance]
noncomputable def category_theory.idempotents.to_karoubi.category_theory.is_equivalence (D : Type u_2) [category_theory.category D] [category_theory.is_idempotent_complete D] :
category_theory.is_equivalence (category_theory.idempotents.to_karoubi D)
Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_counit_iso_hom_app_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (X_1 : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₂ C D).counit_iso.hom.app X).app X_1).f = (category_theory.idempotents.to_karoubi D).inv.map (X.map ((category_theory.idempotents.to_karoubi C).map X_1.p)) ≫ (category_theory.is_equivalence.counit_iso.hom.app (X.obj ((category_theory.idempotents.to_karoubi C).obj X_1.X))).f ≫ (X.map X_1.decomp_id_p).f
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_obj_X (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X).obj P).X = X.obj P.X
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_map_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (_x _x_1 : C ⥤ D) (f : _x ⟶ _x_1) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₂ C D).functor.map f).app P).f = f.app P.X ≫ _x_1.map P.p
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_obj_p (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (P : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X).obj P).p = X.map P.p
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_unit_iso_hom_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal₂ C D).unit_iso.hom.app X).app X_1 = ((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : C ⥤ D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso ≪≫ F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv) _) (category_theory.nat_iso.of_components (λ (F : C ⥤ category_theory.idempotents.karoubi D), F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D) ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso ≪≫ F.right_unitor) _)).hom.app X).app X_1 ≫ (category_theory.idempotents.to_karoubi D).inv.map (category_theory.eq_to_hom _)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_obj_map (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (_x _x_1 : C) (f : _x ⟶ _x_1) :
((category_theory.idempotents.karoubi_universal₂ C D).inverse.obj X).map f = (category_theory.idempotents.to_karoubi D).inv.map (X.map ((category_theory.idempotents.to_karoubi C).map f))
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_functor_obj_map_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (P Q : category_theory.idempotents.karoubi C) (f : P ⟶ Q) :
(((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X).map f).f = X.map f.f
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_counit_iso_inv_app_app_f (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (X_1 : category_theory.idempotents.karoubi C) :
(((category_theory.idempotents.karoubi_universal₂ C D).counit_iso.inv.app X).app X_1).f = (X.map X_1.decomp_id_i).f ≫ (X.map ((category_theory.idempotents.to_karoubi C).map X_1.p)).f ≫ (category_theory.is_equivalence.counit_iso.inv.app (X.obj ((category_theory.idempotents.to_karoubi C).obj X_1.X))).f ≫ 𝟙 ((category_theory.idempotents.to_karoubi D).inv.obj (X.obj ((category_theory.idempotents.to_karoubi C).obj X_1.X)))
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_unit_iso_inv_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal₂ C D).unit_iso.inv.app X).app X_1 = (category_theory.idempotents.to_karoubi D).inv.map (category_theory.eq_to_hom _) ≫ ((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : C ⥤ D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso ≪≫ F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv) _) (category_theory.nat_iso.of_components (λ (F : C ⥤ category_theory.idempotents.karoubi D), F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D) ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso ≪≫ F.right_unitor) _)).inv.app X).app X_1
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_map_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (_x _x_1 : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (f : _x ⟶ _x_1) (X : C) :
((category_theory.idempotents.karoubi_universal₂ C D).inverse.map f).app X = (category_theory.idempotents.to_karoubi D).inv.map (f.app ((category_theory.idempotents.to_karoubi C).obj X))
source
noncomputable def category_theory.idempotents.karoubi_universal₂ (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
C ⥤ D ≌ category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D

The equivalence of categories (C ⥤ D) ≌ (karoubi C ⥤ karoubi D) when D is idempotent complete.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal₂_inverse_obj_obj (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal₂ C D).inverse.obj X).obj X_1 = (category_theory.idempotents.to_karoubi D).inv.obj (X.obj ((category_theory.idempotents.to_karoubi C).obj X_1))
source
theorem category_theory.idempotents.karoubi_universal₂_functor_eq (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
(category_theory.idempotents.karoubi_universal₂ C D).functor = category_theory.idempotents.functor_extension₂ C D
source
@[protected, instance]
noncomputable def category_theory.idempotents.functor_extension₂.category_theory.is_equivalence (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
category_theory.is_equivalence (category_theory.idempotents.functor_extension₂ C D)
Equations
source
@[simp]
theorem category_theory.idempotents.functor_extension_obj_obj (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.functor_extension C D).obj X).obj X_1 = (category_theory.is_equivalence.inverse (category_theory.idempotents.to_karoubi D)).obj (((category_theory.idempotents.functor_extension₂ C D).obj X).obj X_1)
source
noncomputable def category_theory.idempotents.functor_extension (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
(C ⥤ D) ⥤ category_theory.idempotents.karoubi C ⥤ D

The extension of functors functor (C ⥤ D) ⥤ (karoubi C ⥤ D) when D is idempotent compltete.

Equations
Instances for category_theory.idempotents.functor_extension
source
@[simp]
theorem category_theory.idempotents.functor_extension_obj_map (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (_x _x_1 : category_theory.idempotents.karoubi C) (f : _x ⟶ _x_1) :
((category_theory.idempotents.functor_extension C D).obj X).map f = (category_theory.is_equivalence.inverse (category_theory.idempotents.to_karoubi D)).map (((category_theory.idempotents.functor_extension₂ C D).obj X).map f)
source
@[simp]
theorem category_theory.idempotents.functor_extension_map_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (_x _x_1 : C ⥤ D) (f : _x ⟶ _x_1) (X : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.functor_extension C D).map f).app X = (category_theory.is_equivalence.inverse (category_theory.idempotents.to_karoubi D)).map (((category_theory.idempotents.functor_extension₂ C D).map f).app X)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_obj_map (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (_x _x_1 : category_theory.idempotents.karoubi C) (f : _x ⟶ _x_1) :
((category_theory.idempotents.karoubi_universal C D).functor.obj X).map f = (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X).map f)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_map_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (_x _x_1 : category_theory.idempotents.karoubi C ⥤ D) (f : _x ⟶ _x_1) (X : C) :
((category_theory.idempotents.karoubi_universal C D).inverse.map f).app X = category_theory.is_equivalence.unit_iso.inv.app (_x.obj ((category_theory.idempotents.to_karoubi C).obj X)) ≫ f.app ((category_theory.idempotents.to_karoubi C).obj X) ≫ category_theory.is_equivalence.unit_iso.hom.app (_x_1.obj ((category_theory.idempotents.to_karoubi C).obj X))
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_obj_map (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ D) (_x _x_1 : C) (f : _x ⟶ _x_1) :
((category_theory.idempotents.karoubi_universal C D).inverse.obj X).map f = category_theory.is_equivalence.unit_iso.inv.app (X.obj ((category_theory.idempotents.to_karoubi C).obj _x)) ≫ X.map ((category_theory.idempotents.to_karoubi C).map f) ≫ category_theory.is_equivalence.unit_iso.hom.app (X.obj ((category_theory.idempotents.to_karoubi C).obj _x_1))
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_obj_obj (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.karoubi_universal C D).functor.obj X).obj X_1 = (category_theory.idempotents.to_karoubi D).inv.obj (((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X).obj X_1)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_functor_map_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (_x _x_1 : C ⥤ D) (f : _x ⟶ _x_1) (X : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.karoubi_universal C D).functor.map f).app X = (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.idempotents.karoubi_universal₂ C D).functor.map f).app X)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_counit_iso_hom_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ D) (X_1 : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.karoubi_universal C D).counit_iso.hom.app X).app X_1 = (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.idempotents.karoubi_universal₂ C D).counit_iso.hom.app (X ⋙ category_theory.idempotents.to_karoubi D)).app X_1) ≫ category_theory.is_equivalence.unit_iso.inv.app (X.obj X_1)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_inverse_obj_obj (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal C D).inverse.obj X).obj X_1 = (category_theory.idempotents.to_karoubi D).inv.obj ((category_theory.idempotents.to_karoubi D).obj (X.obj ((category_theory.idempotents.to_karoubi C).obj X_1)))
source
noncomputable def category_theory.idempotents.karoubi_universal (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
C ⥤ D ≌ category_theory.idempotents.karoubi C ⥤ D

The equivalence (C ⥤ D) ≌ (karoubi C ⥤ D) when D is idempotent complete.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_counit_iso_inv_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : category_theory.idempotents.karoubi C ⥤ D) (X_1 : category_theory.idempotents.karoubi C) :
((category_theory.idempotents.karoubi_universal C D).counit_iso.inv.app X).app X_1 = category_theory.is_equivalence.unit_iso.hom.app (X.obj X_1) ≫ (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.idempotents.karoubi_universal₂ C D).counit_iso.inv.app (X ⋙ category_theory.idempotents.to_karoubi D)).app X_1)
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_unit_iso_hom_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal C D).unit_iso.hom.app X).app X_1 = ((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : C ⥤ D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso ≪≫ F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv) _) (category_theory.nat_iso.of_components (λ (F : C ⥤ category_theory.idempotents.karoubi D), F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D) ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso ≪≫ F.right_unitor) _)).hom.app X).app X_1 ≫ (category_theory.idempotents.to_karoubi D).inv.map (category_theory.eq_to_hom _) ≫ (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso.symm ≪≫ F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D)) _) (category_theory.nat_iso.of_components (λ (F : category_theory.idempotents.karoubi C ⥤ D), F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso.symm ≪≫ F.right_unitor) _)).hom.app ((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X)).app ((category_theory.idempotents.to_karoubi C).obj X_1))
source
@[simp]
theorem category_theory.idempotents.karoubi_universal_unit_iso_inv_app_app (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] (X : C ⥤ D) (X_1 : C) :
((category_theory.idempotents.karoubi_universal C D).unit_iso.inv.app X).app X_1 = (category_theory.idempotents.to_karoubi D).inv.map (((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : category_theory.idempotents.karoubi C ⥤ category_theory.idempotents.karoubi D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso.symm ≪≫ F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D)) _) (category_theory.nat_iso.of_components (λ (F : category_theory.idempotents.karoubi C ⥤ D), F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso.symm ≪≫ F.right_unitor) _)).inv.app ((category_theory.idempotents.karoubi_universal₂ C D).functor.obj X)).app ((category_theory.idempotents.to_karoubi C).obj X_1)) ≫ (category_theory.idempotents.to_karoubi D).inv.map (category_theory.eq_to_hom _) ≫ ((category_theory.equivalence.adjointify_η (category_theory.nat_iso.of_components (λ (F : C ⥤ D), F.right_unitor.symm ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.unit_iso ≪≫ F.associator (category_theory.idempotents.to_karoubi D) (category_theory.idempotents.to_karoubi D).inv) _) (category_theory.nat_iso.of_components (λ (F : C ⥤ category_theory.idempotents.karoubi D), F.associator (category_theory.idempotents.to_karoubi D).inv (category_theory.idempotents.to_karoubi D) ≪≫ category_theory.iso_whisker_left F category_theory.is_equivalence.counit_iso ≪≫ F.right_unitor) _)).inv.app X).app X_1
source
theorem category_theory.idempotents.karoubi_universal_functor_eq (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
(category_theory.idempotents.karoubi_universal C D).functor = category_theory.idempotents.functor_extension C D
source
@[protected, instance]
noncomputable def category_theory.idempotents.functor_extension.category_theory.is_equivalence (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
category_theory.is_equivalence (category_theory.idempotents.functor_extension C D)
Equations
source
@[protected, instance]
noncomputable def category_theory.idempotents.obj.category_theory.is_equivalence (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] :
category_theory.is_equivalence ((category_theory.whiskering_left C (category_theory.idempotents.karoubi C) D).obj (category_theory.idempotents.to_karoubi C))
Equations
source
theorem category_theory.idempotents.whiskering_left_obj_preimage_app {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.is_idempotent_complete D] {F G : category_theory.idempotents.karoubi C ⥤ D} (τ : category_theory.idempotents.to_karoubi C ⋙ F ⟶ category_theory.idempotents.to_karoubi C ⋙ G) (P : category_theory.idempotents.karoubi C) :
(((category_theory.whiskering_left C (category_theory.idempotents.karoubi C) D).obj (category_theory.idempotents.to_karoubi C)).preimage τ).app P = F.map P.decomp_id_i ≫ τ.app P.X ≫ G.map P.decomp_id_p