mathlib documentation

category_theory.adjunction.fully_faithful

@[instance]

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

See

@[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.

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.

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

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