# 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).

## Future work #

The statements from Riehl 4.5.13 for adjoints which are either full, or faithful.

instance CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Full] [L.Faithful] :

If the left adjoint is fully faithful, then the unit is an isomorphism.

See

Equations
• =
instance CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Full] [R.Faithful] :

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!)

Equations
• =
@[simp]
theorem CategoryTheory.Adjunction.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.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] (X : C) :
h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)
@[simp]
theorem CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] (X : C) :
h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)
noncomputable def CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] :
L.comp (R.comp L) L

If the unit is an isomorphism, bundle one has an isomorphism L ⋙ R ⋙ L ≅ L.

Equations
Instances For
@[simp]
theorem CategoryTheory.Adjunction.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.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] (X : D) :
h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)
@[simp]
theorem CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] (X : D) :
h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)
noncomputable def CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] :
R.comp (L.comp R) R

If the counit of an is an isomorphism, one has an isomorphism (R ⋙ L ⋙ R) ≅ R.

Equations
• h.whiskerLeftRUnitIsoOfIsIsoCounit = (R.associator L R).symm ≪≫ ≪≫ R.leftUnitor
Instances For
noncomputable def CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.unit] :
L.FullyFaithful

If the unit is an isomorphism, then the left adjoint is fully faithful.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [CategoryTheory.IsIso h.counit] :
R.FullyFaithful

If the counit is an isomorphism, then the right adjoint is fully faithful.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Full] [L.Faithful] :
Equations
• =
instance CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Full] [L.Faithful] :
Equations
• =
instance CategoryTheory.Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Full] [R.Faithful] :
Equations
• =
instance CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Full] [R.Faithful] :
Equations
• =
instance CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Faithful] [L.Full] {Y : C} :
CategoryTheory.IsIso (h.counit.app (L.obj Y))
Equations
• =
instance CategoryTheory.Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Faithful] [L.Full] {Y : D} :
CategoryTheory.IsIso (R.map (h.counit.app Y))
Equations
• =
theorem CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Faithful] [L.Full] {X : D} :
CategoryTheory.IsIso (h.counit.app X) X L.essImage
theorem CategoryTheory.Adjunction.isIso_counit_app_of_iso {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.Faithful] [L.Full] {X : D} {Y : C} (e : X L.obj Y) :
CategoryTheory.IsIso (h.counit.app X)
instance CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Faithful] [R.Full] {Y : D} :
CategoryTheory.IsIso (h.unit.app (R.obj Y))
Equations
• =
instance CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Faithful] [R.Full] {X : C} :
CategoryTheory.IsIso (L.map (h.unit.app X))
Equations
• =
theorem CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Faithful] [R.Full] {Y : C} :
CategoryTheory.IsIso (h.unit.app Y) Y R.essImage
theorem CategoryTheory.Adjunction.isIso_unit_app_of_iso {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y R.obj X) :
CategoryTheory.IsIso (h.unit.app Y)
instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.IsEquivalence] :
Equations
• =
instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.IsEquivalence] :
Equations
• =
theorem CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.IsEquivalence] :
L.IsEquivalence
theorem CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.IsEquivalence] :
R.IsEquivalence
instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1 {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [L.IsEquivalence] :
Equations
• =
instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1 {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) [R.IsEquivalence] :
Equations
• =