Documentation

Mathlib.CategoryTheory.Adjunction.FullyFaithful

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.

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

See

Equations
  • =

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₁} [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.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₁} [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) :
h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)
@[simp]
theorem CategoryTheory.Adjunction.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) :
h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)

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₁} [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.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₁} [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) :
    h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)
    @[simp]
    theorem CategoryTheory.Adjunction.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) :
    h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)

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

    Equations
    Instances For

      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

        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
          Equations
          • =
          Equations
          • =
          theorem CategoryTheory.Adjunction.isIso_counit_app_of_iso {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) [L.Faithful] [L.Full] {X : D} {Y : C} (e : X L.obj Y) :
          CategoryTheory.IsIso (h.counit.app X)
          Equations
          • =
          Equations
          • =
          theorem CategoryTheory.Adjunction.isIso_unit_app_of_iso {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) [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y R.obj X) :
          CategoryTheory.IsIso (h.unit.app Y)