Documentation

Mathlib.CategoryTheory.Adjunction.Restrict

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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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) :
    CategoryTheory.CategoryStruct.comp (iC.map ((adj.restrictFullyFaithful hiC hiD 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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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) = 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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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) :
    CategoryTheory.CategoryStruct.comp (iD.map ((adj.restrictFullyFaithful hiC hiD 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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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) = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))
    theorem CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply {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') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.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 (CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryTheory.CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))