Restricting adjunctions

Adjunction.restrictFullyFaithful shows that an adjunction can be restricted along fully faithful inclusions.

noncomputable def CategoryTheory.Adjunction.restrictFullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (iC : CategoryTheory.Functor C C') (iD : CategoryTheory.Functor D D') {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] : L ⊣ R

If C is a full subcategory of C' and D is a full subcategory of D', then we can restrict an adjunction L' ⊣ R' where L' : C' ⥤ D' and R' : D' ⥤ C' to C and D. The construction here is slightly more general, in that C is required only to have a full and faithful "inclusion" functor iC : C ⥤ C' (and similarly iD : D ⥤ D') which commute (up to natural isomorphism) with the proposed restrictions.

Equations

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

theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (iC : CategoryTheory.Functor C C') (iD : CategoryTheory.Functor D D') {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] (X : C) {Z : C'} (h : iC.obj (R.obj (L.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (iC.map ((CategoryTheory.Adjunction.restrictFullyFaithful iC iD adj comm1 comm2).unit.app X)) h = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryTheory.CategoryStruct.comp (comm2.hom.app (L.obj X)) h))

@[simp]

theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (iC : CategoryTheory.Functor C C') (iD : CategoryTheory.Functor D D') {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] (X : C) : iC.map ((CategoryTheory.Adjunction.restrictFullyFaithful iC iD adj comm1 comm2).unit.app X) = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (comm2.hom.app (L.obj X)))

theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (iC : CategoryTheory.Functor C C') (iD : CategoryTheory.Functor D D') {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] (X : D) {Z : D'} (h : iD.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (iD.map ((CategoryTheory.Adjunction.restrictFullyFaithful iC iD adj comm1 comm2).counit.app X)) h = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (CategoryTheory.CategoryStruct.comp (adj.counit.app (iD.obj X)) h))

@[simp]

theorem CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (iC : CategoryTheory.Functor C C') (iD : CategoryTheory.Functor D D') {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] (X : D) : iD.map ((CategoryTheory.Adjunction.restrictFullyFaithful iC iD adj comm1 comm2).counit.app X) = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))