mathlibdocumentation

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

We provide various useful constructors:

• mk_of_hom_equiv
• mk_of_unit_counit
• left_adjoint_of_equiv / right_adjoint_of equiv construct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.
• adjunction_of_equiv_left / adjunction_of_equiv_right witness that these constructions give adjunctions.

There are also typeclasses is_left_adjoint / is_right_adjoint, carrying data witnessing that a given functor is a left or right adjoint. Given [is_left_adjoint F], a right adjoint of F can be constructed as right_adjoint F.

adjunction.comp composes adjunctions.

to_equivalence upgrades an adjunction to an equivalence, given witnesses that the unit and counit are pointwise isomorphisms. Conversely equivalence.to_adjunction recovers the underlying adjunction from an equivalence.

structure category_theory.adjunction {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) :
Type (max u₁ u₂ v₁ v₂)

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

To construct an adjunction between two functors, it's often easier to instead use the constructors mk_of_hom_equiv or mk_of_unit_counit. To construct a left adjoint, there are also constructors left_adjoint_of_equiv and adjunction_of_equiv_left (as well as their duals) which can be simpler in practice.

Uniqueness of adjoints is shown in category_theory.adjunction.opposites.

Instances for category_theory.adjunction
@[class]
structure category_theory.is_left_adjoint {C : Type u₁} {D : Type u₂} (left : C D) :
Type (max u₁ u₂ v₁ v₂)
• right : D C

A class giving a chosen right adjoint to the functor left.

Instances of this typeclass
Instances of other typeclasses for category_theory.is_left_adjoint
@[class]
structure category_theory.is_right_adjoint {C : Type u₁} {D : Type u₂} (right : D C) :
Type (max u₁ u₂ v₁ v₂)
• left : C D

A class giving a chosen left adjoint to the functor right.

Instances of this typeclass
Instances of other typeclasses for category_theory.is_right_adjoint
def category_theory.left_adjoint {C : Type u₁} {D : Type u₂} (R : D C)  :
C D

Equations
def category_theory.right_adjoint {C : Type u₁} {D : Type u₂} (L : C D)  :
D C

Equations
def category_theory.adjunction.of_left_adjoint {C : Type u₁} {D : Type u₂} (left : C D)  :
left

The adjunction associated to a functor known to be a left adjoint.

Equations
def category_theory.adjunction.of_right_adjoint {C : Type u₁} {D : Type u₂} (right : C D)  :
right

The adjunction associated to a functor known to be a right adjoint.

Equations
@[simp]
theorem category_theory.adjunction.hom_equiv_unit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : F G) {X : C} {Y : D} {f : F.obj X Y} :
(self.hom_equiv X Y) f = self.unit.app X G.map f
@[simp]
theorem category_theory.adjunction.hom_equiv_counit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : F G) {X : C} {Y : D} {g : X G.obj Y} :
((self.hom_equiv X Y).symm) g = F.map g self.counit.app Y
theorem category_theory.adjunction.hom_equiv_id {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) (X : C) :
theorem category_theory.adjunction.hom_equiv_symm_id {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) (X : D) :
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_left_symm {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
((adj.hom_equiv X' Y).symm) (f g) = F.map f ((adj.hom_equiv X Y).symm) g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_left {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
(adj.hom_equiv X' Y) (F.map f g) = f (adj.hom_equiv X Y) g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_right {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X : C} {Y Y' : D} (f : F.obj X Y) (g : Y Y') :
(adj.hom_equiv X Y') (f g) = (adj.hom_equiv X Y) f G.map g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_right_symm {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
((adj.hom_equiv X Y').symm) (f G.map g) = ((adj.hom_equiv X Y).symm) f g
@[simp]
theorem category_theory.adjunction.left_triangle {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) :
@[simp]
theorem category_theory.adjunction.right_triangle {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) :
@[simp]
theorem category_theory.adjunction.left_triangle_components {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X : C} :
@[simp]
theorem category_theory.adjunction.left_triangle_components_assoc {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X : C} {X' : D} (f' : (𝟭 D).obj (F.obj X) X') :
@[simp]
theorem category_theory.adjunction.right_triangle_components {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {Y : D} :
@[simp]
theorem category_theory.adjunction.right_triangle_components_assoc {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {Y : D} {X' : C} (f' : G.obj ((𝟭 D).obj Y) X') :
@[simp]
theorem category_theory.adjunction.counit_naturality_assoc {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : D} (f : X Y) {X' : D} (f' : (𝟭 D).obj Y X') :
@[simp]
theorem category_theory.adjunction.counit_naturality {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : D} (f : X Y) :
@[simp]
theorem category_theory.adjunction.unit_naturality_assoc {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : C} (f : X Y) {X' : C} (f' : G.obj (F.obj Y) X') :
@[simp]
theorem category_theory.adjunction.unit_naturality {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : C} (f : X Y) :
theorem category_theory.adjunction.hom_equiv_apply_eq {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
(adj.hom_equiv A B) f = g f = ((adj.hom_equiv A B).symm) g
theorem category_theory.adjunction.eq_hom_equiv_apply {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
g = (adj.hom_equiv A B) f ((adj.hom_equiv A B).symm) g = f
@[nolint]
structure category_theory.adjunction.core_hom_equiv {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) :
Type (max u₁ u₂ v₁ v₂)

This is an auxiliary data structure useful for constructing adjunctions. See adjunction.mk_of_hom_equiv. This structure won't typically be used anywhere else.

Instances for category_theory.adjunction.core_hom_equiv
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : G) {X' X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
((self.hom_equiv X' Y).symm) (f g) = F.map f ((self.hom_equiv X Y).symm) g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : G) {X : C} {Y Y' : D} (f : F.obj X Y) (g : Y Y') :
(self.hom_equiv X Y') (f g) = (self.hom_equiv X Y) f G.map g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
(adj.hom_equiv X' Y) (F.map f g) = f (adj.hom_equiv X Y) g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right_symm {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
((adj.hom_equiv X Y').symm) (f G.map g) = ((adj.hom_equiv X Y).symm) f g
@[nolint]
structure category_theory.adjunction.core_unit_counit {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) :
Type (max u₁ u₂ v₁ v₂)

This is an auxiliary data structure useful for constructing adjunctions. See adjunction.mk_of_unit_counit. This structure won't typically be used anywhere else.

Instances for category_theory.adjunction.core_unit_counit
@[simp]
theorem category_theory.adjunction.core_unit_counit.left_triangle {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : G) :
(F.associator G F).hom =
@[simp]
theorem category_theory.adjunction.core_unit_counit.right_triangle {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (self : G) :
(G.associator F G).inv =
@[simp]
theorem category_theory.adjunction.mk_of_hom_equiv_unit_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (X : C) :
= (adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X))
def category_theory.adjunction.mk_of_hom_equiv {C : Type u₁} {D : Type u₂} {F : C D} {G : D C}  :
F G

Construct an adjunction between F and G out of a natural bijection between each F.obj X ⟶ Y and X ⟶ G.obj Y.

Equations
@[simp]
theorem category_theory.adjunction.mk_of_hom_equiv_hom_equiv {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (X : C) (Y : D) :
@[simp]
theorem category_theory.adjunction.mk_of_hom_equiv_counit_app {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (Y : D) :
= (adj.hom_equiv (G.obj Y) ((𝟭 D).obj Y)).inv_fun (𝟙 (G.obj Y))
def category_theory.adjunction.mk_of_unit_counit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C}  :
F G

Construct an adjunction between functors F and G given a unit and counit for the adjunction satisfying the triangle identities.

Equations
@[simp]
theorem category_theory.adjunction.mk_of_unit_counit_hom_equiv_symm_apply {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (X : C) (Y : D) (g : X G.obj Y) :
.symm) g = F.map g adj.counit.app Y
@[simp]
theorem category_theory.adjunction.mk_of_unit_counit_unit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C}  :
@[simp]
theorem category_theory.adjunction.mk_of_unit_counit_counit {C : Type u₁} {D : Type u₂} {F : C D} {G : D C}  :
@[simp]
theorem category_theory.adjunction.mk_of_unit_counit_hom_equiv_apply {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (X : C) (Y : D) (f : F.obj X Y) :
f = adj.unit.app X G.map f
def category_theory.adjunction.id {C : Type u₁}  :

The adjunction between the identity functor on a category and itself.

Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_symm_apply {C : Type u₁} {D : Type u₂} {F F' : C D} (iso : F F') {X : C} {Y : D} (g : F'.obj X Y) :
= iso.hom.app X g
def category_theory.adjunction.equiv_homset_left_of_nat_iso {C : Type u₁} {D : Type u₂} {F F' : C D} (iso : F F') {X : C} {Y : D} :
(F.obj X Y) (F'.obj X Y)

If F and G are naturally isomorphic functors, establish an equivalence of hom-sets.

Equations
@[simp]
theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_apply {C : Type u₁} {D : Type u₂} {F F' : C D} (iso : F F') {X : C} {Y : D} (f : F.obj X Y) :
= iso.inv.app X f
@[simp]
theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_apply {C : Type u₁} {D : Type u₂} {G G' : D C} (iso : G G') {X : C} {Y : D} (f : X G.obj Y) :
= f iso.hom.app Y
def category_theory.adjunction.equiv_homset_right_of_nat_iso {C : Type u₁} {D : Type u₂} {G G' : D C} (iso : G G') {X : C} {Y : D} :
(X G.obj Y) (X G'.obj Y)

If G and H are naturally isomorphic functors, establish an equivalence of hom-sets.

Equations
@[simp]
theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_symm_apply {C : Type u₁} {D : Type u₂} {G G' : D C} (iso : G G') {X : C} {Y : D} (g : X G'.obj Y) :
= g iso.inv.app Y
def category_theory.adjunction.of_nat_iso_left {C : Type u₁} {D : Type u₂} {F G : C D} {H : D C} (adj : F H) (iso : F G) :
G H

Transport an adjunction along an natural isomorphism on the left.

Equations
def category_theory.adjunction.of_nat_iso_right {C : Type u₁} {D : Type u₂} {F : C D} {G H : D C} (adj : F G) (iso : G H) :
F H

Transport an adjunction along an natural isomorphism on the right.

Equations
def category_theory.adjunction.right_adjoint_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

Transport being a right adjoint along a natural isomorphism.

Equations
def category_theory.adjunction.left_adjoint_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

Transport being a left adjoint along a natural isomorphism.

Equations
def category_theory.adjunction.comp {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} {E : Type u₃} [ℰ : category_theory.category E] {H : D E} {I : E D} (adj₁ : F G) (adj₂ : H I) :
F H I G

Equations
@[protected, instance]
def category_theory.adjunction.left_adjoint_of_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

If F and G are left adjoints then F ⋙ G is a left adjoint too.

Equations
@[protected, instance]
def category_theory.adjunction.right_adjoint_of_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] {F : C D} {G : D E}  :

If F and G are right adjoints then F ⋙ G is a right adjoint too.

Equations
@[simp]
theorem category_theory.adjunction.left_adjoint_of_equiv_obj {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) (ᾰ : C) :
= F_obj ᾰ
@[simp]
theorem category_theory.adjunction.left_adjoint_of_equiv_map {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) (X X' : C) (f : X X') :
= ((e X (F_obj X')).symm) (f (e X' (F_obj X')) (𝟙 (F_obj X')))
def category_theory.adjunction.left_adjoint_of_equiv {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) :
C D

Construct a left adjoint functor to G, given the functor's value on objects F_obj and a bijection e between F_obj X ⟶ Y and X ⟶ G.obj Y satisfying a naturality law he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g. Dual to right_adjoint_of_equiv.

Equations
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_unit_app {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) (X : C) :
= (e X (F_obj X)) (𝟙 (F_obj X))
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_counit_app {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) (Y : D) :
= ((e (G.obj Y) Y).symm) (𝟙 (G.obj Y))
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_hom_equiv {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) (X : C) (Y : D) :
= e X Y
def category_theory.adjunction.adjunction_of_equiv_left {C : Type u₁} {D : Type u₂} {G : D C} {F_obj : C → D} (e : Π (X : C) (Y : D), (F_obj X Y) (X G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y Y') (h : F_obj X Y), (e X Y') (h g) = (e X Y) h G.map g) :

Show that the functor given by left_adjoint_of_equiv is indeed left adjoint to G. Dual to adjunction_of_equiv_right.

Equations
def category_theory.adjunction.right_adjoint_of_equiv {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) :
D C

Construct a right adjoint functor to F, given the functor's value on objects G_obj and a bijection e between F.obj X ⟶ Y and X ⟶ G_obj Y satisfying a naturality law he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g. Dual to left_adjoint_of_equiv.

Equations
@[simp]
theorem category_theory.adjunction.right_adjoint_of_equiv_obj {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) (ᾰ : D) :
= G_obj ᾰ
@[simp]
theorem category_theory.adjunction.right_adjoint_of_equiv_map {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) (Y Y' : D) (g : Y Y') :
= (e (G_obj Y) Y') (((e (G_obj Y) Y).symm) (𝟙 (G_obj Y)) g)
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_hom_equiv {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) (X : C) (Y : D) :
= e X Y
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_counit_app {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) (Y : D) :
= ((e (G_obj Y) Y).symm) (𝟙 (G_obj Y))
def category_theory.adjunction.adjunction_of_equiv_right {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) :

Show that the functor given by right_adjoint_of_equiv is indeed right adjoint to F. Dual to adjunction_of_equiv_left.

Equations
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_unit_app {C : Type u₁} {D : Type u₂} {F : C D} {G_obj : D → C} (e : Π (X : C) (Y : D), (F.obj X Y) (X G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' X) (g : F.obj X Y), (e X' Y) (F.map f g) = f (e X Y) g) (X : C) :
= (e X (F.obj X)) (𝟙 (F.obj X))
@[simp]
theorem category_theory.adjunction.to_equivalence_inverse {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) [∀ (X : C), category_theory.is_iso (adj.unit.app X)] [∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
@[simp]
theorem category_theory.adjunction.to_equivalence_functor {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) [∀ (X : C), category_theory.is_iso (adj.unit.app X)] [∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
@[simp]
theorem category_theory.adjunction.to_equivalence_unit_iso {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) [∀ (X : C), category_theory.is_iso (adj.unit.app X)] [∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
@[simp]
theorem category_theory.adjunction.to_equivalence_counit_iso {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) [∀ (X : C), category_theory.is_iso (adj.unit.app X)] [∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
noncomputable def category_theory.adjunction.to_equivalence {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) [∀ (X : C), category_theory.is_iso (adj.unit.app X)] [∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
C D

If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the adjunction to an equivalence.

Equations
@[simp]
theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_inverse {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] :
@[simp]
theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_hom_app {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] (X : C) :
@[simp]
theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_inv_app {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] (X : C) :
noncomputable def category_theory.adjunction.is_right_adjoint_to_is_equivalence {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] :

If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise) isomorphisms, then the functor is an equivalence of categories.

Equations
@[simp]
theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_unit_iso_hom_app {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] (X : D) :
@[simp]
theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_unit_iso_inv_app {C : Type u₁} {D : Type u₂} {G : D C} [∀ (X : C), ] [∀ (Y : D), ] (X : D) :
def category_theory.equivalence.to_adjunction {C : Type u₁} {D : Type u₂} (e : C D) :

The adjunction given by an equivalence of categories. (To obtain the opposite adjunction, simply use e.symm.to_adjunction.

Equations
@[simp]
theorem category_theory.equivalence.as_equivalence_to_adjunction_unit {C : Type u₁} {D : Type u₂} {e : C D} :
@[simp]
theorem category_theory.equivalence.as_equivalence_to_adjunction_counit {C : Type u₁} {D : Type u₂} {e : C D} :
def category_theory.functor.adjunction {C : Type u₁} {D : Type u₂} (E : C D)  :
E E.inv

An equivalence E is left adjoint to its inverse.

Equations
@[protected, instance]
def category_theory.functor.left_adjoint_of_equivalence {C : Type u₁} {D : Type u₂} {F : C D}  :

If F is an equivalence, it's a left adjoint.

Equations
@[simp]
theorem category_theory.functor.right_adjoint_of_is_equivalence {C : Type u₁} {D : Type u₂} {F : C D}  :
@[protected, instance]
def category_theory.functor.right_adjoint_of_equivalence {C : Type u₁} {D : Type u₂} {F : C D}  :

If F is an equivalence, it's a right adjoint.

Equations
@[simp]
theorem category_theory.functor.left_adjoint_of_is_equivalence {C : Type u₁} {D : Type u₂} {F : C D}  :