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.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.Functor.Full L] [CategoryTheory.Functor.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
  • ⋯ = ⋯
source
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.Functor.Full R] [CategoryTheory.Functor.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
  • ⋯ = ⋯
source
@[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.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.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.obj X)
source
@[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.map (h.unit.app X)
source
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.
Instances For
    source
    @[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.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.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.map (h.counit.app X)
    source
    @[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.obj X)
    source
    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.
    Instances For
      source
      theorem CategoryTheory.L_full_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.Functor.Full L

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

      source
      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.Functor.Faithful L

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

      source
      theorem CategoryTheory.R_full_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.Functor.Full R

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

      source
      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.Functor.Faithful R

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

      source
      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.Functor.Full L] [CategoryTheory.Functor.Faithful L] :
      CategoryTheory.IsIso (CategoryTheory.whiskerLeft L h.counit)
      Equations
      • ⋯ = ⋯
      source
      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.Functor.Full L] [CategoryTheory.Functor.Faithful L] :
      CategoryTheory.IsIso (CategoryTheory.whiskerRight h.counit R)
      Equations
      • ⋯ = ⋯
      source
      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.Functor.Full R] [CategoryTheory.Functor.Faithful R] :
      CategoryTheory.IsIso (CategoryTheory.whiskerLeft R h.unit)
      Equations
      • ⋯ = ⋯
      source
      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.Functor.Full R] [CategoryTheory.Functor.Faithful R] :
      CategoryTheory.IsIso (CategoryTheory.whiskerRight h.unit L)
      Equations
      • ⋯ = ⋯
      source
      instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToPrefunctorCompObjToQuiverToCategoryStructToPrefunctorIdAppCounit {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.Functor.Faithful L] [CategoryTheory.Functor.Full L] {Y : C} :
      CategoryTheory.IsIso (h.counit.app (L.obj Y))
      Equations
      • ⋯ = ⋯
      source
      theorem CategoryTheory.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) [CategoryTheory.Functor.Faithful L] [CategoryTheory.Functor.Full L] {X : D} :
      CategoryTheory.IsIso (h.counit.app X) ↔ X ∈ CategoryTheory.Functor.essImage L
      source
      theorem CategoryTheory.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) [CategoryTheory.Functor.Faithful L] [CategoryTheory.Functor.Full L] {X : D} {Y : C} (e : X ≅ L.obj Y) :
      CategoryTheory.IsIso (h.counit.app X)
      source
      instance CategoryTheory.instIsIsoObjToQuiverToCategoryStructToPrefunctorIdObjToQuiverToCategoryStructToPrefunctorCompAppUnit {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.Functor.Faithful R] [CategoryTheory.Functor.Full R] {Y : D} :
      CategoryTheory.IsIso (h.unit.app (R.obj Y))
      Equations
      • ⋯ = ⋯
      source
      theorem CategoryTheory.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) [CategoryTheory.Functor.Faithful R] [CategoryTheory.Functor.Full R] {Y : C} :
      CategoryTheory.IsIso (h.unit.app Y) ↔ Y ∈ CategoryTheory.Functor.essImage R
      source
      theorem CategoryTheory.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) [CategoryTheory.Functor.Faithful R] [CategoryTheory.Functor.Full R] {X : D} {Y : C} (e : Y ≅ R.obj X) :
      CategoryTheory.IsIso (h.unit.app Y)