Documentation

Mathlib.CategoryTheory.Adjunction.FullyFaithful

Adjoints of fully faithful functors #

A left adjoint is

A right adjoint is

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.

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

Equations
  • β‹― = β‹―

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

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

    Equations
    • β‹― = β‹―
    Equations
    • β‹― = β‹―

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

    Equations
    • β‹― = β‹―

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

    Equations
    • β‹― = β‹―

    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

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

      Equations
      • β‹― = β‹―
      Equations
      • β‹― = β‹―

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

      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 each component of the unit is a monomorphism, then the left adjoint is faithful.

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

          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 each component of the counit is an epimorphism, then the right adjoint is faithful.

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

            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
              • β‹― = β‹―

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

              @[deprecated CategoryTheory.Adjunction.mem_essImage_of_unit_isIso]

              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₁} [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)