Adjoints of fully faithful functors

A left adjoint is

• faithful, if and only if the unit is a monomorphism
• full, if and only if the unit is a split epimorphism
• fully faithful, if and only if the unit is an isomorphism

A right adjoint is

• faithful, if and only if the counit is an epimorphism
• full, if and only if the counit is a split monomorphism
• fully faithful, if and only if the counit is an isomorphism

This is Lemma 4.5.13 in Riehl's Category Theory in Context [riehl2017]. See also https://stacks.math.columbia.edu/tag/07RB for the statements about fully faithful functors.

In the file Mathlib/CategoryTheory/Monad/Adjunction.lean, we prove that in fact, if there exists an isomorphism L ⋙ R ≅ 𝟭 C, then the unit is an isomorphism, and similarly for the counit. See CategoryTheory.Adjunction.isIso_unit_of_iso and CategoryTheory.Adjunction.isIso_counit_of_iso.

instance CategoryTheory.Adjunction.unit_mono_of_L_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Faithful] (X : C) : Mono (h.unit.app X)

If the left adjoint is faithful, then each component of the unit is an monomorphism.

noncomputable def CategoryTheory.Adjunction.unitSplitEpiOfLFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] (X : C) : SplitEpi (h.unit.app X)

If the left adjoint is full, then each component of the unit is a split epimorphism.

instance CategoryTheory.Adjunction.unit_isSplitEpi_of_L_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] (X : C) : IsSplitEpi (h.unit.app X)

If the right adjoint is full, then each component of the counit is a split monomorphism.

instance CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful] (X : C) : IsIso (h.unit.app X)

instance CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful] : IsIso h.unit

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

instance CategoryTheory.Adjunction.counit_epi_of_R_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Faithful] (X : D) : Epi (h.counit.app X)

If the right adjoint is faithful, then each component of the counit is an epimorphism.

noncomputable def CategoryTheory.Adjunction.counitSplitMonoOfRFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] (X : D) : SplitMono (h.counit.app X)

If the right adjoint is full, then each component of the counit is a split monomorphism.

instance CategoryTheory.Adjunction.counit_isSplitMono_of_R_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] (X : D) : IsSplitMono (h.counit.app X)

If the right adjoint is full, then each component of the counit is a split monomorphism.

instance CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful] (X : D) : IsIso (h.counit.app X)

instance CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful] : IsIso h.counit

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

@[simp]

theorem CategoryTheory.Adjunction.inv_map_unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) {X : C} [IsIso (h.unit.app X)] : 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.

noncomputable def CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.unit] : L.comp (R.comp L) ≅ L

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

@[simp]

theorem CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.unit] (X : C) : h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)

@[simp]

theorem CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.unit] (X : C) : h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)

@[simp]

theorem CategoryTheory.Adjunction.inv_counit_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) {X : D} [IsIso (h.counit.app X)] : 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.

noncomputable def CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [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.

@[simp]

theorem CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.counit] (X : D) : h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)

@[simp]

theorem CategoryTheory.Adjunction.whiskerLeftRUnitIsoOfIsIsoCounit_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.counit] (X : D) : h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)

theorem CategoryTheory.Adjunction.faithful_L_of_mono_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [∀ (X : C), Mono (h.unit.app X)] : L.Faithful

If each component of the unit is a monomorphism, then the left adjoint is faithful.

theorem CategoryTheory.Adjunction.full_L_of_isSplitEpi_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [∀ (X : C), IsSplitEpi (h.unit.app X)] : L.Full

If each component of the unit is a split epimorphism, then the left adjoint is full.

noncomputable def CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.unit] : L.FullyFaithful

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

theorem CategoryTheory.Adjunction.faithful_R_of_epi_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [∀ (X : D), Epi (h.counit.app X)] : R.Faithful

If each component of the counit is an epimorphism, then the right adjoint is faithful.

theorem CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [∀ (X : D), IsSplitMono (h.counit.app X)] : R.Full

If each component of the counit is a split monomorphism, then the right adjoint is full.

noncomputable def CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [IsIso h.counit] : R.FullyFaithful

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

instance CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful] : IsIso (L.whiskerLeft h.counit)

instance CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful] : IsIso (Functor.whiskerRight h.counit R)

instance CategoryTheory.Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful] : IsIso (R.whiskerLeft h.unit)

instance CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful] : IsIso (Functor.whiskerRight h.unit L)

instance CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {Y : C} : IsIso (h.counit.app (L.obj Y))

instance CategoryTheory.Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {Y : D} : IsIso (R.map (h.counit.app Y))

theorem CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {X : D} : IsIso (h.counit.app X) ↔ L.essImage X

theorem CategoryTheory.Adjunction.mem_essImage_of_counit_isIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) (A : D) [IsIso (h.counit.app A)] : L.essImage A

theorem CategoryTheory.Adjunction.isIso_counit_app_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {X : D} {Y : C} (e : X ≅ L.obj Y) : IsIso (h.counit.app X)

instance CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {Y : D} : IsIso (h.unit.app (R.obj Y))

instance CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {X : C} : IsIso (L.map (h.unit.app X))

theorem CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {Y : C} : IsIso (h.unit.app Y) ↔ R.essImage Y

theorem CategoryTheory.Adjunction.mem_essImage_of_unit_isIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) (A : C) [IsIso (h.unit.app A)] : R.essImage A

If η_A is an isomorphism, then A is in the essential image of i.

theorem CategoryTheory.Adjunction.isIso_unit_app_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y ≅ R.obj X) : IsIso (h.unit.app Y)

instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.IsEquivalence] : IsIso h.unit

instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.IsEquivalence] : IsIso h.counit

theorem CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.IsEquivalence] : L.IsEquivalence

theorem CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.IsEquivalence] : R.IsEquivalence

instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [L.IsEquivalence] : IsIso h.unit

instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (h : L ⊣ R) [R.IsEquivalence] : IsIso h.counit