# 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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] (X : C) :
.app X = h.counit.app (L.obj X)
@[simp]
theorem CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] (X : C) :
.app X = L.map (h.unit.app X)
noncomputable def CategoryTheory.whiskerLeftLCounitIsoOfIsIsoUnit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] (X : D) :
.app X = R.map (h.counit.app X)
@[simp]
theorem CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] (X : D) :
.app X = h.unit.app (R.obj X)
noncomputable def CategoryTheory.whiskerLeftRUnitIsoOfIsIsoCounit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
instance CategoryTheory.whiskerLeft_unit_iso_of_R_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
instance CategoryTheory.whiskerRight_unit_iso_of_R_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
def CategoryTheory.Adjunction.restrictFullyFaithful {C : Type u₁} [] {D : Type u₂} [] {C' : Type u₃} [] {D' : Type u₄} [] (iC : ) (iD : ) {L' : } {R' : } (adj : L' R') {L : } {R : } (comm1 : ) (comm2 : ) [] [] :
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.

Instances For