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

Equations

• (_ : CategoryTheory.IsIso h.unit) = (_ : CategoryTheory.IsIso h.unit)

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 (we only prove the forward direction!)

Equations

• (_ : CategoryTheory.IsIso h.counit) = (_ : CategoryTheory.IsIso h.counit)

@[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.toPrefunctor.map (h.unit.app X)) = h.counit.app (L.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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] : CategoryTheory.Functor.comp L (CategoryTheory.Functor.comp R L) ≅ L

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

Equations

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

@[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.toPrefunctor.map (h.counit.app X)) = h.unit.app (R.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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] : CategoryTheory.Functor.comp R (CategoryTheory.Functor.comp L R) ≅ R

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

Equations

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

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] : CategoryTheory.Full L

If the unit is an isomorphism, then the left adjoint is full

Equations

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

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] : CategoryTheory.Faithful L

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] : CategoryTheory.Full R

If the counit is an isomorphism, then the right adjoint is full

Equations

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

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] : CategoryTheory.Faithful R

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)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.whiskerLeft L h.counit)) = (_ : 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)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.whiskerRight h.counit R)) = (_ : 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)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.whiskerLeft R h.unit)) = (_ : 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)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.whiskerRight h.unit L)) = (_ : 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.

Equations

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