mathlib documentation

category_theory.adjunction.fully_faithful

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).

adjunction.restrict_fully_faithful shows that an adjunction can be restricted along fully faithful inclusions.

Future work #

The statements from Riehl 4.5.13 for adjoints which are either full, or faithful.

@[protected, instance]

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

See

@[protected, instance]

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!)

@[simp]
theorem category_theory.inv_map_unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) {X : C} [category_theory.is_iso (h.unit.app 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.

noncomputable def category_theory.whisker_left_L_counit_iso_of_is_iso_unit {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.is_iso h.unit] :
L R L L

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

Equations
@[simp]
theorem category_theory.inv_counit_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) {X : D} [category_theory.is_iso (h.counit.app 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.

noncomputable def category_theory.whisker_left_R_unit_iso_of_is_iso_counit {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.is_iso h.counit] :
R L R R

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

Equations
noncomputable def category_theory.L_full_of_unit_is_iso {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.is_iso h.unit] :

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

Equations

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

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

Equations

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

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