Restricting adjunctions

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

noncomputable def CategoryTheory.Adjunction.restrictFullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] {iC : Functor C C'} {iD : Functor D D'} {L' : Functor C' D'} {R' : Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : Functor C D} {R : Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) : 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.

@[simp]

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

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

@[simp]

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

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

theorem CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u₃} [Category.{v₃, u₃} C'] {D' : Type u₄} [Category.{v₄, u₄} D'] {iC : Functor C C'} {iD : Functor D D'} {L' : Functor C' D'} {R' : Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : Functor C D} {R : Functor D C} (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) {X : C} {Y : D} (f : L.obj X ⟶ Y) : ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f = hiC.preimage (CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))