mathlib3 documentation

category_theory.adjunction.fully_faithful

Adjoints of fully faithful functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[protected, 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

source
@[protected, 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!)

source
@[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)] :
category_theory.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 category_theory.whisker_left_L_counit_iso_of_is_iso_unit_hom_app {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] (X : C) :
(category_theory.whisker_left_L_counit_iso_of_is_iso_unit h).hom.app X = h.counit.app (L.obj X)
source
@[simp]
theorem category_theory.whisker_left_L_counit_iso_of_is_iso_unit_inv_app {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] (X : C) :
(category_theory.whisker_left_L_counit_iso_of_is_iso_unit h).inv.app X = L.map (h.unit.app X)
source
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
source
@[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)] :
category_theory.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 category_theory.whisker_left_R_unit_iso_of_is_iso_counit_hom_app {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] (X : D) :
(category_theory.whisker_left_R_unit_iso_of_is_iso_counit h).hom.app X = R.map (h.counit.app X)
source
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
source
@[simp]
theorem category_theory.whisker_left_R_unit_iso_of_is_iso_counit_inv_app {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] (X : D) :
(category_theory.whisker_left_R_unit_iso_of_is_iso_counit h).inv.app X = h.unit.app (R.obj X)
source
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] :
category_theory.full L

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

Equations
source
theorem category_theory.L_faithful_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] :
category_theory.faithful L

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

source
noncomputable def category_theory.R_full_of_counit_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.counit] :
category_theory.full R

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

Equations
source
theorem category_theory.R_faithful_of_counit_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.counit] :
category_theory.faithful R

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

source
@[protected, instance]
def category_theory.whisker_left_counit_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 (category_theory.whisker_left L h.counit)
source
@[protected, instance]
def category_theory.whisker_right_counit_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 (category_theory.whisker_right h.counit R)
source
@[protected, instance]
def category_theory.whisker_left_unit_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 (category_theory.whisker_left R h.unit)
source
@[protected, instance]
def category_theory.whisker_right_unit_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 (category_theory.whisker_right h.unit L)
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