Adjoints of fully faithful functors #
A left adjoint is fully faithful, if and only if the unit is an isomorphism (and similarly for right adjoints and the counit).
Adjunction.restrictFullyFaithful shows that an adjunction can be restricted along fully faithful
inclusions.
Future work #
The statements from Riehl 4.5.13 for adjoints which are either full, or faithful.
instance
CategoryTheory.unit_isIso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full L]
[CategoryTheory.Faithful L]
:
CategoryTheory.IsIso h.unit
If the left adjoint is fully faithful, then the unit is an isomorphism.
See
- Lemma 4.5.13 from [Riehl][riehl2017]
- https://math.stackexchange.com/a/2727177
- https://stacks.math.columbia.edu/tag/07RB (we only prove the forward direction!)
instance
CategoryTheory.counit_isIso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full R]
[CategoryTheory.Faithful R]
:
CategoryTheory.IsIso h.counit
If the right adjoint is fully faithful, then the counit is an isomorphism.
See https://stacks.math.columbia.edu/tag/07RB (we only prove the forward direction!)
@[simp]
theorem
CategoryTheory.inv_map_unit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
{X : C}
[CategoryTheory.IsIso (h.unit.app X)]
:
CategoryTheory.inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)
If the unit of an adjunction is an isomorphism, then its inverse on the image of L is given by L whiskered with the counit.
@[simp]
theorem
CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
(X : C)
:
(CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit h).hom.app X = h.counit.app (L.obj X)
@[simp]
theorem
CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
(X : C)
:
(CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit h).inv.app X = L.map (h.unit.app X)
noncomputable def
CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
:
If the unit is an isomorphism, bundle one has an isomorphism L ⋙ R ⋙ L ≅ L.
Instances For
@[simp]
theorem
CategoryTheory.inv_counit_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
{X : D}
[CategoryTheory.IsIso (h.counit.app X)]
:
CategoryTheory.inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)
If the counit of an adjunction is an isomorphism, then its inverse on the image of R is given by R whiskered with the unit.
@[simp]
theorem
CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
(X : D)
:
(CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit h).hom.app X = R.map (h.counit.app X)
@[simp]
theorem
CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
(X : D)
:
(CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit h).inv.app X = h.unit.app (R.obj X)
noncomputable def
CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
:
If the counit of an is an isomorphism, one has an isomorphism (R ⋙ L ⋙ R) ≅ R.
Instances For
noncomputable def
CategoryTheory.lFullOfUnitIsIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
:
If the unit is an isomorphism, then the left adjoint is full
Instances For
theorem
CategoryTheory.L_faithful_of_unit_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.unit]
:
If the unit is an isomorphism, then the left adjoint is faithful
noncomputable def
CategoryTheory.rFullOfCounitIsIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
:
If the counit is an isomorphism, then the right adjoint is full
Instances For
theorem
CategoryTheory.R_faithful_of_counit_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.IsIso h.counit]
:
If the counit is an isomorphism, then the right adjoint is faithful
instance
CategoryTheory.whiskerLeft_counit_iso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full L]
[CategoryTheory.Faithful L]
:
CategoryTheory.IsIso (CategoryTheory.whiskerLeft L h.counit)
instance
CategoryTheory.whiskerRight_counit_iso_of_L_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full L]
[CategoryTheory.Faithful L]
:
CategoryTheory.IsIso (CategoryTheory.whiskerRight h.counit R)
instance
CategoryTheory.whiskerLeft_unit_iso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full R]
[CategoryTheory.Faithful R]
:
CategoryTheory.IsIso (CategoryTheory.whiskerLeft R h.unit)
instance
CategoryTheory.whiskerRight_unit_iso_of_R_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(h : L ⊣ R)
[CategoryTheory.Full R]
[CategoryTheory.Faithful R]
:
CategoryTheory.IsIso (CategoryTheory.whiskerRight h.unit L)
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.Full iC]
[CategoryTheory.Faithful iC]
[CategoryTheory.Full iD]
[CategoryTheory.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.