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, carrying data witnessing that a given functor is a left or right adjoint. Given [IsLeftAdjoint F], a right adjoint of F can be constructed as rightAdjoint F.

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

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

    Instances For
      class CategoryTheory.IsLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (left : CategoryTheory.Functor C D) :
      Type (max (max (max u₁ u₂) v₁) v₂)

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

      Instances
        class CategoryTheory.IsRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (right : CategoryTheory.Functor D C) :
        Type (max (max (max u₁ u₂) v₁) v₂)

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

        Instances

          Extract the left adjoint from the instance giving the chosen adjoint.

          Instances For

            Extract the right adjoint from the instance giving the chosen adjoint.

            Instances For

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

              Instances For

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

                Instances For
                  @[simp]
                  @[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) :
                  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) :

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

                  Instances For

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

                    Instances For

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

                      Instances For

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

                        Instances For

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

                          Instances For

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

                            Instances For

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

                              Instances For

                                Transport an adjunction along a natural isomorphism on the left.

                                Instances For

                                  Transport an adjunction along a natural isomorphism on the right.

                                  Instances For

                                    Transport being a left adjoint along a natural isomorphism.

                                    Instances For
                                      @[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'))))
                                      @[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
                                      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.

                                      Instances For
                                        @[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))
                                        @[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_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) :
                                        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.

                                        Instances For
                                          @[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
                                          @[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') :
                                          (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).map g = ↑(e (G_obj Y) Y') (CategoryTheory.CategoryStruct.comp ((e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))) g)
                                          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.

                                          Instances For
                                            @[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) :
                                            @[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) :
                                            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.

                                            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) :
                                              (CategoryTheory.Adjunction.toEquivalence adj).counitIso.hom.app X = adj.counit.app X
                                              @[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) :
                                              (CategoryTheory.Adjunction.toEquivalence adj).counitIso.inv.app X = CategoryTheory.inv (adj.counit.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) :
                                              (CategoryTheory.Adjunction.toEquivalence adj).unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)
                                              @[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) :
                                              (CategoryTheory.Adjunction.toEquivalence adj).unitIso.hom.app X = 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.

                                              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.

                                                Instances For

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

                                                  Instances For