mathlib documentation

category_theory.adjunction.fully_faithful

source
@[instance]
def category_theory.unit_is_iso_of_L_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) [category_theory.full L] [category_theory.faithful L] :
category_theory.is_iso 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]
def category_theory.counit_is_iso_of_R_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) [category_theory.full R] [category_theory.faithful R] :
category_theory.is_iso 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
def category_theory.adjunction.restrict_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {C' : Type u₃} [category_theory.category C'] {D' : Type u₄} [category_theory.category D'] (iC : C ⥤ C') (iD : D ⥤ D') {L' : C' ⥤ D'} {R' : D' ⥤ C'} (adj : L' ⊣ R') {L : C ⥤ D} {R : D ⥤ C} (comm1 : iC ⋙ L' ≅ L ⋙ iD) (comm2 : iD ⋙ R' ≅ R ⋙ iC) [category_theory.full iC] [category_theory.faithful iC] [category_theory.full iD] [category_theory.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