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 : CategoryTheory.Functor.comp iC L' ≅ CategoryTheory.Functor.comp L iD)
(comm2 : CategoryTheory.Functor.comp iD R' ≅ CategoryTheory.Functor.comp R iC)
[CategoryTheory.Functor.Full iC]
[CategoryTheory.Functor.Faithful iC]
[CategoryTheory.Functor.Full iD]
[CategoryTheory.Functor.Faithful iD]
:
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')
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(comm1 : CategoryTheory.Functor.comp iC L' ≅ CategoryTheory.Functor.comp L iD)
(comm2 : CategoryTheory.Functor.comp iD R' ≅ CategoryTheory.Functor.comp R iC)
[CategoryTheory.Functor.Full iC]
[CategoryTheory.Functor.Faithful iC]
[CategoryTheory.Functor.Full iD]
[CategoryTheory.Functor.Faithful iD]
(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 : CategoryTheory.Functor.comp iC L' ≅ CategoryTheory.Functor.comp L iD)
(comm2 : CategoryTheory.Functor.comp iD R' ≅ CategoryTheory.Functor.comp R iC)
[CategoryTheory.Functor.Full iC]
[CategoryTheory.Functor.Faithful iC]
[CategoryTheory.Functor.Full iD]
[CategoryTheory.Functor.Faithful iD]
(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 : CategoryTheory.Functor.comp iC L' ≅ CategoryTheory.Functor.comp L iD)
(comm2 : CategoryTheory.Functor.comp iD R' ≅ CategoryTheory.Functor.comp R iC)
[CategoryTheory.Functor.Full iC]
[CategoryTheory.Functor.Faithful iC]
[CategoryTheory.Functor.Full iD]
[CategoryTheory.Functor.Faithful iD]
(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 : CategoryTheory.Functor.comp iC L' ≅ CategoryTheory.Functor.comp L iD)
(comm2 : CategoryTheory.Functor.comp iD R' ≅ CategoryTheory.Functor.comp R iC)
[CategoryTheory.Functor.Full iC]
[CategoryTheory.Functor.Faithful iC]
[CategoryTheory.Functor.Full iD]
[CategoryTheory.Functor.Faithful iD]
(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)))