Documentation

Mathlib.CategoryTheory.Adjunction.FullyFaithful

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 [Rie17]. See also https://stacks.math.columbia.edu/tag/07RB for the statements about fully faithful functors.

In the file Mathlib.CategoryTheory.Monad.Adjunction, 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.

Equations

h.unitSplitEpiOfLFull X = { section_ := L.preimage (h.counit.app (L.obj X)), id := ⋯ }

Instances For

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.

Equations

h.counitSplitMonoOfRFull X = { retraction := R.preimage (h.unit.app (R.obj X)), id := ⋯ }

Instances For

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.

Equations

h.whiskerLeftLCounitIsoOfIsIsoUnit = (L.associator R L).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.asIso h.unit).symm L ≪≫ L.leftUnitor

Instances For

@[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.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.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.

Equations

h.whiskerLeftRUnitIsoOfIsIsoCounit = (R.associator L R).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.asIso h.counit) R ≪≫ R.leftUnitor

Instances For

@[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)

@[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)

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

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.

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₁} [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 (whiskerLeft L 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 (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 (whiskerLeft R 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 (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) ↔ X ∈ L.essImage

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)] :

A ∈ L.essImage

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) ↔ Y ∈ R.essImage

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)] :

A ∈ R.essImage

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

@[deprecated CategoryTheory.Adjunction.mem_essImage_of_unit_isIso (since := "2024-06-19")]

theorem CategoryTheory.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)] :

A ∈ R.essImage

Alias of CategoryTheory.Adjunction.mem_essImage_of_unit_isIso.

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