Documentation

Mathlib.CategoryTheory.Adjunction.Basic

Adjunctions between functors #

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:

There are also typeclasses IsLeftAdjoint / IsRightAdjoint, which asserts the existence of a adjoint functor. Given [F.IsLeftAdjoint], a chosen right adjoint can be obtained as F.rightAdjoint.

Adjunction.comp composes adjunctions.

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

structure CategoryTheory.Adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) :
Type (max (max (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 mkOfHomEquiv or mkOfUnitCounit. To construct a left adjoint, there are also constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as well as their duals) which can be simpler in practice.

Uniqueness of adjoints is shown in CategoryTheory.Adjunction.Opposites.

See https://stacks.math.columbia.edu/tag/0037.

Instances For
    @[simp]
    theorem CategoryTheory.Adjunction.homEquiv_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F G) {X : C} {Y : D} {f : F.obj X Y} :
    (self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)

    Naturality of the unit of an adjunction

    @[simp]
    theorem CategoryTheory.Adjunction.homEquiv_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F G) {X : C} {Y : D} {g : X G.obj Y} :
    (self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)

    Naturality of the counit of an adjunction

    The notation F ⊣ G stands for Adjunction F G representing that F is left adjoint to G

    Equations
    Instances For

      A class asserting the existence of a right adjoint.

      Instances

        A class asserting the existence of a left adjoint.

        Instances

          A chosen left adjoint to a functor that is a right adjoint.

          Equations
          • R.leftAdjoint = .choose
          Instances For

            A chosen right adjoint to a functor that is a left adjoint.

            Equations
            • L.rightAdjoint = .choose
            Instances For
              noncomputable def CategoryTheory.Adjunction.ofIsLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (left : CategoryTheory.Functor C D) [left.IsLeftAdjoint] :
              left left.rightAdjoint

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

              Equations
              Instances For
                noncomputable def CategoryTheory.Adjunction.ofIsRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (right : CategoryTheory.Functor C D) [right.IsRightAdjoint] :
                right.leftAdjoint right

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

                Equations
                Instances For
                  Equations
                  • =
                  Equations
                  • =
                  theorem CategoryTheory.Adjunction.homEquiv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (X : C) :
                  (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) = adj.unit.app X
                  theorem CategoryTheory.Adjunction.homEquiv_symm_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (X : D) :
                  (adj.homEquiv (G.obj X) X).symm (CategoryTheory.CategoryStruct.id (G.obj X)) = adj.counit.app X
                  @[simp]
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_left_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
                  (adj.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)
                  @[simp]
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
                  (adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
                  @[simp]
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X : C} {Y : D} {Y' : D} (f : F.obj X Y) (g : Y Y') :
                  (adj.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)
                  @[simp]
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_right_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X : C} {Y : D} {Y' : D} (f : X G.obj Y) (g : Y Y') :
                  (adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : F.obj X Y') (h : F.obj X' Y) (k : Y Y') (w : CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h✝ k) {Z : C} (h : G.obj Y' Z) :
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : F.obj X Y') (h : F.obj X' Y) (k : Y Y') (w : CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k) :
                  CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k)
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h✝ (G.map k)) {Z : D} (h : Y' Z) :
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)) :
                  CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : F.obj X Y') (h : F.obj X' Y) (k : Y Y') :
                  theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X' : C} {X : C} {Y : D} {Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') :
                  @[simp]
                  theorem CategoryTheory.Adjunction.left_triangle_components_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (X : C) {Z : D} (h : F.obj X Z) :
                  CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj X)) h) = h
                  @[simp]
                  theorem CategoryTheory.Adjunction.right_triangle_components_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) (Y : D) {Z : C} (h : G.obj Y Z) :
                  CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (CategoryTheory.CategoryStruct.comp (G.map (adj.counit.app Y)) h) = h
                  @[simp]
                  theorem CategoryTheory.Adjunction.counit_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X : D} {Y : D} (f : X Y) :
                  CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (adj.counit.app Y) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) f
                  @[simp]
                  theorem CategoryTheory.Adjunction.unit_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {X : C} {Y : C} (f : X Y) :
                  CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) = CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)
                  theorem CategoryTheory.Adjunction.homEquiv_apply_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
                  (adj.homEquiv A B) f = g f = (adj.homEquiv A B).symm g
                  theorem CategoryTheory.Adjunction.eq_homEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
                  g = (adj.homEquiv A B) f (adj.homEquiv A B).symm g = f

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

                  Instances For
                    @[simp]
                    theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' : C} {X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
                    (self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)

                    The property that describes how homEquiv.symm transforms compositions X' ⟶ X ⟶ G Y

                    @[simp]

                    The property that describes how homEquiv transforms compositions F X ⟶ Y ⟶ Y'

                    @[simp]
                    theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_aux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' : C} {X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
                    CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' (F.obj X)) (F.map f)) (G.map g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
                    @[simp]
                    theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm_aux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X : C} {Y : D} {Y' : D} (f : X G.obj Y) (g : Y Y') :
                    CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv (G.obj Y) Y').symm (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g

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

                    Instances For
                      @[simp]

                      Equality of the composition of the unit, associator, and counit with the identity F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F

                      @[simp]

                      Equality of the composition of the unit, associator, and counit with the identity G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id 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
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • CategoryTheory.Adjunction.instInhabitedId = { default := CategoryTheory.Adjunction.id }

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Transport an adjunction along a natural isomorphism on the left.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Transport an adjunction along a natural isomorphism on the right.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Composition of adjunctions.

                                    See https://stacks.math.columbia.edu/tag/0DV0.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem CategoryTheory.Adjunction.comp_unit_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F G) (adj₂ : H I) (X : C) {Z : C} (h : G.obj (I.obj (H.obj (F.obj X))) Z) :
                                      CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).unit.app X) h = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (adj₂.unit.app (F.obj X))) h)
                                      @[simp]
                                      theorem CategoryTheory.Adjunction.comp_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F G) (adj₂ : H I) (X : C) :
                                      (adj₁.comp adj₂).unit.app X = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (G.map (adj₂.unit.app (F.obj X)))
                                      theorem CategoryTheory.Adjunction.comp_counit_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F G) (adj₂ : H I) (X : E) {Z : E} (h : X Z) :
                                      CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).counit.app X) h = CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (CategoryTheory.CategoryStruct.comp (adj₂.counit.app X) h)
                                      @[simp]
                                      theorem CategoryTheory.Adjunction.comp_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F G) (adj₂ : H I) (X : E) :
                                      (adj₁.comp adj₂).counit.app X = CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (adj₂.counit.app X)
                                      @[simp]
                                      theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) :
                                      ∀ (a : C), (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a = F_obj a
                                      @[simp]
                                      theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) {X : C} {X' : C} (f : X X') :
                                      (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).map f = (e X (F_obj X')).symm (CategoryTheory.CategoryStruct.comp f ((e X' (F_obj X')) (CategoryTheory.CategoryStruct.id (F_obj X'))))
                                      def CategoryTheory.Adjunction.leftAdjointOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) :

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (X : C) :
                                        @[simp]
                                        theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (X : C) (Y : D) :
                                        @[simp]
                                        theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (Y : D) :
                                        (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).counit.app Y = (e (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
                                        def CategoryTheory.Adjunction.adjunctionOfEquivLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : CD} (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') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) :

                                        Show that the functor given by leftAdjointOfEquiv is indeed left adjoint to G. Dual to adjunctionOfRightEquiv.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) {Y : D} {Y' : D} (g : Y Y') :
                                          @[simp]
                                          theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) :
                                          ∀ (a : D), (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a = G_obj a
                                          def CategoryTheory.Adjunction.rightAdjointOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) :

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

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (Y : D) :
                                            (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).counit.app Y = (e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))
                                            @[simp]
                                            theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (X : C) (Y : D) :
                                            @[simp]
                                            theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (X : C) :
                                            def CategoryTheory.Adjunction.adjunctionOfEquivRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : DC} (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) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) :

                                            Show that the functor given by rightAdjointOfEquiv is indeed right adjoint to F. Dual to adjunctionOfEquivRight.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D) :
                                              adj.toEquivalence.counitIso.hom.app X = adj.counit.app X
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] :
                                              adj.toEquivalence.functor = F
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D) :
                                              adj.toEquivalence.counitIso.inv.app X = CategoryTheory.inv (adj.counit.app X)
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] :
                                              adj.toEquivalence.inverse = G
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_unitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C) :
                                              adj.toEquivalence.unitIso.hom.app X = adj.unit.app X
                                              @[simp]
                                              theorem CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C) :
                                              adj.toEquivalence.unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)
                                              noncomputable def CategoryTheory.Adjunction.toEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                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.

                                                @[simp]
                                                @[simp]

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

                                                Equations
                                                Instances For
                                                  instance CategoryTheory.Functor.isLeftAdjoint_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsLeftAdjoint] [G.IsLeftAdjoint] :
                                                  (F.comp G).IsLeftAdjoint

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

                                                  Equations
                                                  • =
                                                  instance CategoryTheory.Functor.isRightAdjoint_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.IsRightAdjoint] [G.IsRightAdjoint] :
                                                  (F.comp G).IsRightAdjoint

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

                                                  Equations
                                                  • =

                                                  Transport being a right adjoint along a natural isomorphism.

                                                  Transport being a left adjoint along a natural isomorphism.

                                                  An equivalence E is left adjoint to its inverse.

                                                  Equations
                                                  • E.adjunction = E.asEquivalence.toAdjunction
                                                  Instances For
                                                    @[instance 10]

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

                                                    Equations
                                                    • =
                                                    @[instance 10]

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

                                                    Equations
                                                    • =