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.

source
instance CategoryTheory.Adjunction.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) [L.Full] [L.Faithful] :
CategoryTheory.IsIso h.unit

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

See

Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Adjunction.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) [R.Full] [R.Faithful] :
CategoryTheory.IsIso h.counit

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
  • ⋯ = ⋯
source
@[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.

source
@[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)
source
@[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)
source
noncomputable def CategoryTheory.Adjunction.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] :
L.comp (R.comp L) ≅ L

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

Equations
Instances For
    source
    @[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.

    source
    @[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)
    source
    @[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)
    source
    noncomputable def CategoryTheory.Adjunction.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] :
    R.comp (L.comp R) ≅ R

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

    Equations
    Instances For
      source
      noncomputable def CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit {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] :
      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
        source
        noncomputable def CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit {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] :
        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
          source
          instance CategoryTheory.Adjunction.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) [L.Full] [L.Faithful] :
          CategoryTheory.IsIso (CategoryTheory.whiskerLeft L h.counit)
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.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) [L.Full] [L.Faithful] :
          CategoryTheory.IsIso (CategoryTheory.whiskerRight h.counit R)
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.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) [R.Full] [R.Faithful] :
          CategoryTheory.IsIso (CategoryTheory.whiskerLeft R h.unit)
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.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) [R.Full] [R.Faithful] :
          CategoryTheory.IsIso (CategoryTheory.whiskerRight h.unit L)
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull {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] {Y : C} :
          CategoryTheory.IsIso (h.counit.app (L.obj Y))
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull {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] {Y : D} :
          CategoryTheory.IsIso (R.map (h.counit.app Y))
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage {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} :
          CategoryTheory.IsIso (h.counit.app X) ↔ X ∈ L.essImage
          source
          theorem CategoryTheory.Adjunction.mem_essImage_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) (A : D) [CategoryTheory.IsIso (h.counit.app A)] :
          A ∈ L.essImage
          source
          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)
          source
          instance CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull {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] {Y : D} :
          CategoryTheory.IsIso (h.unit.app (R.obj Y))
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull {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 : C} :
          CategoryTheory.IsIso (L.map (h.unit.app X))
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage {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] {Y : C} :
          CategoryTheory.IsIso (h.unit.app Y) ↔ Y ∈ R.essImage
          source
          theorem CategoryTheory.Adjunction.mem_essImage_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) (A : C) [CategoryTheory.IsIso (h.unit.app A)] :
          A ∈ R.essImage

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

          source
          @[deprecated CategoryTheory.Adjunction.mem_essImage_of_unit_isIso]
          theorem CategoryTheory.mem_essImage_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) (A : C) [CategoryTheory.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.

          source
          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)
          source
          instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence {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.IsEquivalence] :
          CategoryTheory.IsIso h.unit
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence {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.IsEquivalence] :
          CategoryTheory.IsIso h.counit
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right {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.IsEquivalence] :
          L.IsEquivalence
          source
          theorem CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left {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.IsEquivalence] :
          R.IsEquivalence
          source
          instance CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1 {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.IsEquivalence] :
          CategoryTheory.IsIso h.unit
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1 {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.IsEquivalence] :
          CategoryTheory.IsIso h.counit
          Equations
          • ⋯ = ⋯