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.

Overview of the directory CategoryTheory.Adjunction #

structure CategoryTheory.Adjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (G : 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.

We use the unit-counit definition of an adjunction. There is a constructor Adjunction.mk' which constructs an adjunction from the data of a hom set equivalence, a unit, and a counit, together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other.

There is also a constructor Adjunction.mkOfHomEquiv which constructs an adjunction from a natural hom set equivalence.

To construct adjoints to a given functor, there are constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as well as their duals).

Instances For

    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
              Instances For

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

                Equations
                  Instances For
                    noncomputable def CategoryTheory.Adjunction.ofIsLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (left : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (right : Functor C D) [right.IsRightAdjoint] :
                        right.leftAdjoint right

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

                        Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Adjunction.left_triangle_components_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (self : F G) (X : C) {Z : D} (h : F.obj X Z) :
                            @[simp]
                            theorem CategoryTheory.Adjunction.right_triangle_components_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (self : F G) (Y : D) {Z : C} (h : G.obj Y Z) :
                            def CategoryTheory.Adjunction.homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) (Y : D) :
                            (F.obj X Y) (X G.obj Y)

                            The hom set equivalence associated to an adjunction.

                            Equations
                              Instances For
                                theorem CategoryTheory.Adjunction.homEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) (Y : D) (f : F.obj X Y) :
                                (adj.homEquiv X Y) f = CategoryStruct.comp (adj.unit.app X) (G.map f)
                                theorem CategoryTheory.Adjunction.homEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) (Y : D) (g : X G.obj Y) :
                                (adj.homEquiv X Y).symm g = CategoryStruct.comp (F.map g) (adj.counit.app Y)
                                theorem CategoryTheory.Adjunction.homEquiv_unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) (Y : D) (f : F.obj X Y) :
                                (adj.homEquiv X Y) f = CategoryStruct.comp (adj.unit.app X) (G.map f)

                                Alias of CategoryTheory.Adjunction.homEquiv_apply.

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

                                Alias of CategoryTheory.Adjunction.homEquiv_symm_apply.

                                theorem CategoryTheory.Adjunction.ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {adj adj' : F G} (h : adj.unit = adj'.unit) :
                                adj = adj'
                                theorem CategoryTheory.Adjunction.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {adj adj' : F G} :
                                adj = adj' adj.unit = adj'.unit
                                theorem CategoryTheory.Adjunction.homEquiv_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) :
                                (adj.homEquiv X (F.obj X)) (CategoryStruct.id (F.obj X)) = adj.unit.app X
                                theorem CategoryTheory.Adjunction.homEquiv_symm_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : D) :
                                (adj.homEquiv (G.obj X) X).symm (CategoryStruct.id (G.obj X)) = adj.counit.app X
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_left_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
                                (adj.homEquiv X' Y).symm (CategoryStruct.comp f g) = CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
                                (adj.homEquiv X' Y) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((adj.homEquiv X Y) g)
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X : C} {Y Y' : D} (f : F.obj X Y) (g : Y Y') :
                                (adj.homEquiv X Y') (CategoryStruct.comp f g) = CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_right_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
                                (adj.homEquiv X Y').symm (CategoryStruct.comp f (G.map g)) = CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y Y' : D} (f : X' X) (g : F.obj X Y') (h : F.obj X' Y) (k : Y Y') (w : CategoryStruct.comp (F.map f) g = CategoryStruct.comp h k) :
                                CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k)
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y Y' : D} (f : X' X) (g : F.obj X Y') (h : F.obj X' Y) (k : Y Y') (w : CategoryStruct.comp (F.map f) g = CategoryStruct.comp h k) {Z : C} (h✝ : G.obj Y' Z) :
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') (w : CategoryStruct.comp f g = CategoryStruct.comp h (G.map k)) :
                                CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') (w : CategoryStruct.comp f g = CategoryStruct.comp h (G.map k)) {Z : D} (h✝ : Y' Z) :
                                theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X' X : C} {Y Y' : D} (f : X' X) (g : X G.obj Y') (h : X' G.obj Y) (k : Y Y') :
                                @[simp]
                                theorem CategoryTheory.Adjunction.counit_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X Y : D} (f : X Y) :
                                @[simp]
                                theorem CategoryTheory.Adjunction.counit_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X Y : D} (f : X Y) {Z : D} (h : Y Z) :
                                @[simp]
                                theorem CategoryTheory.Adjunction.unit_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X Y : C} (f : X Y) :
                                @[simp]
                                theorem CategoryTheory.Adjunction.unit_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {X Y : C} (f : X Y) {Z : C} (h : G.obj (F.obj Y) Z) :
                                theorem CategoryTheory.Adjunction.unit_comp_map_eq_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
                                theorem CategoryTheory.Adjunction.eq_unit_comp_map_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
                                theorem CategoryTheory.Adjunction.homEquiv_apply_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : 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
                                def CategoryTheory.Adjunction.corepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) :

                                If adj : F ⊣ G, and X : C, then F.obj X corepresents Y ↦ (X ⟶ G.obj Y).

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Adjunction.corepresentableBy_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : C) {Y✝ : D} :
                                    def CategoryTheory.Adjunction.representableBy {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (Y : D) :

                                    If adj : F ⊣ G, and Y : D, then G.obj Y represents X ↦ (F.obj X ⟶ Y).

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Adjunction.representableBy_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (Y : D) {X✝ : C} :
                                        (adj.representableBy Y).homEquiv = (adj.homEquiv X✝ Y).symm
                                        structure CategoryTheory.Adjunction.CoreHomEquivUnitCounit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (G : Functor D C) :
                                        Type (max (max (max u₁ u₂) v₁) v₂)

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

                                        Instances For
                                          structure CategoryTheory.Adjunction.CoreHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (G : Functor D C) :
                                          Type (max (max (max u₁ u₂) v₁) v₂)

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

                                          Instances For
                                            theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquiv F G) {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
                                            (adj.homEquiv X' Y) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((adj.homEquiv X Y) g)
                                            theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquiv F G) {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
                                            (adj.homEquiv X Y').symm (CategoryStruct.comp f (G.map g)) = CategoryStruct.comp ((adj.homEquiv X Y).symm f) g
                                            structure CategoryTheory.Adjunction.CoreUnitCounit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (G : Functor D C) :
                                            Type (max (max (max u₁ u₂) v₁) v₂)

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

                                            Instances For
                                              def CategoryTheory.Adjunction.mk' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquivUnitCounit F G) :
                                              F G

                                              Construct an adjunction from the data of a CoreHomEquivUnitCounit, i.e. a hom set equivalence, unit and counit natural transformations together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Adjunction.mk'_counit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquivUnitCounit F G) :
                                                  (mk' adj).counit = adj.counit
                                                  @[simp]
                                                  theorem CategoryTheory.Adjunction.mk'_unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquivUnitCounit F G) :
                                                  (mk' adj).unit = adj.unit
                                                  def CategoryTheory.Adjunction.mkOfHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquiv F G) :
                                                  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
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Adjunction.mkOfHomEquiv_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquiv F G) (X : C) :
                                                      (mkOfHomEquiv adj).unit.app X = (adj.homEquiv X (F.obj X)) (CategoryStruct.id (F.obj X))
                                                      @[simp]
                                                      theorem CategoryTheory.Adjunction.mkOfHomEquiv_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : CoreHomEquiv F G) (Y : D) :
                                                      (mkOfHomEquiv adj).counit.app Y = (adj.homEquiv (G.obj Y) Y).symm (CategoryStruct.id (G.obj Y))

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

                                                      Equations
                                                        Instances For

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

                                                          Equations
                                                            Instances For
                                                              def CategoryTheory.Adjunction.equivHomsetLeftOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor 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
                                                                Instances For
                                                                  @[simp]
                                                                  theorem CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (iso : F F') {X : C} {Y : D} (g : F'.obj X Y) :
                                                                  @[simp]
                                                                  theorem CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} (iso : F F') {X : C} {Y : D} (f : F.obj X Y) :
                                                                  def CategoryTheory.Adjunction.equivHomsetRightOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : Functor 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
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem CategoryTheory.Adjunction.equivHomsetRightOfNatIso_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : Functor D C} (iso : G G') {X : C} {Y : D} (f : X G.obj Y) :
                                                                      @[simp]
                                                                      theorem CategoryTheory.Adjunction.equivHomsetRightOfNatIso_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G G' : Functor D C} (iso : G G') {X : C} {Y : D} (g : X G'.obj Y) :
                                                                      def CategoryTheory.Adjunction.ofNatIsoLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {H : Functor D C} (adj : F H) (iso : F G) :
                                                                      G H

                                                                      Transport an adjunction along a natural isomorphism on the left.

                                                                      Equations
                                                                        Instances For
                                                                          def CategoryTheory.Adjunction.ofNatIsoRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G H : Functor D C} (adj : F G) (iso : G H) :
                                                                          F H

                                                                          Transport an adjunction along a natural isomorphism on the right.

                                                                          Equations
                                                                            Instances For

                                                                              The isomorpism which an adjunction F ⊣ G induces on G ⋙ yoneda. This states that Adjunction.homEquiv is natural in both arguments.

                                                                              Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem CategoryTheory.Adjunction.compYonedaIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : D) (X✝ : Cᵒᵖ) (a✝ : ((G.comp yoneda).obj X).obj X✝) :
                                                                                  (adj.compYonedaIso.hom.app X).app X✝ a✝ = CategoryStruct.comp (F.map a✝) (adj.counit.app X)
                                                                                  @[simp]
                                                                                  theorem CategoryTheory.Adjunction.compYonedaIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : D) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.comp ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op)).obj X).obj X✝) :
                                                                                  (adj.compYonedaIso.inv.app X).app X✝ a✝ = CategoryStruct.comp (adj.unit.app (Opposite.unop X✝)) (G.map a✝)

                                                                                  The isomorpism which an adjunction F ⊣ G induces on F.op ⋙ coyoneda. This states that Adjunction.homEquiv is natural in both arguments.

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem CategoryTheory.Adjunction.compCoyonedaIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : Cᵒᵖ) (X✝ : D) (a✝ : ((F.op.comp coyoneda).obj X).obj X✝) :
                                                                                      (adj.compCoyonedaIso.hom.app X).app X✝ a✝ = CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map a✝)
                                                                                      @[simp]
                                                                                      theorem CategoryTheory.Adjunction.compCoyonedaIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) (X : Cᵒᵖ) (X✝ : D) (a✝ : ((coyoneda.comp ((Functor.whiskeringLeft D C (Type v₁)).obj G)).obj X).obj X✝) :
                                                                                      (adj.compCoyonedaIso.inv.app X).app X✝ a✝ = CategoryStruct.comp (F.map a✝) (adj.counit.app X✝)
                                                                                      def CategoryTheory.Adjunction.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) :
                                                                                      F.comp H I.comp G

                                                                                      Composition of adjunctions.

                                                                                      Stacks Tag 0DV0

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.Adjunction.comp_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) (X : C) :
                                                                                          (adj₁.comp adj₂).unit.app X = CategoryStruct.comp (adj₁.unit.app X) (G.map (adj₂.unit.app (F.obj X)))
                                                                                          theorem CategoryTheory.Adjunction.comp_unit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) (X : C) {Z : C} (h : G.obj (I.obj (H.obj (F.obj X))) Z) :
                                                                                          CategoryStruct.comp ((adj₁.comp adj₂).unit.app X) h = CategoryStruct.comp (adj₁.unit.app X) (CategoryStruct.comp (G.map (adj₂.unit.app (F.obj X))) h)
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.Adjunction.comp_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) (X : E) :
                                                                                          (adj₁.comp adj₂).counit.app X = CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (adj₂.counit.app X)
                                                                                          theorem CategoryTheory.Adjunction.comp_counit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) (X : E) {Z : E} (h : X Z) :
                                                                                          CategoryStruct.comp ((adj₁.comp adj₂).counit.app X) h = CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (CategoryStruct.comp (adj₂.counit.app X) h)
                                                                                          theorem CategoryTheory.Adjunction.comp_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} {E : Type u₃} [ : Category.{v₃, u₃} E] {H : Functor D E} {I : Functor E D} (adj₁ : F G) (adj₂ : H I) :
                                                                                          (adj₁.comp adj₂).homEquiv = fun (x : C) (x_1 : E) => (adj₂.homEquiv (F.obj x) x_1).trans (adj₁.homEquiv x (I.obj x_1))
                                                                                          def CategoryTheory.Adjunction.leftAdjointOfEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = 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
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = CategoryStruct.comp ((e X Y) h) (G.map g)) {X X' : C} (f : X X') :
                                                                                              (leftAdjointOfEquiv e he).map f = (e X (F_obj X')).symm (CategoryStruct.comp f ((e X' (F_obj X')) (CategoryStruct.id (F_obj X'))))
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = CategoryStruct.comp ((e X Y) h) (G.map g)) (a✝ : C) :
                                                                                              (leftAdjointOfEquiv e he).obj a✝ = F_obj a✝
                                                                                              def CategoryTheory.Adjunction.adjunctionOfEquivLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = 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.adjunctionOfEquivLeft_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = CategoryStruct.comp ((e X Y) h) (G.map g)) (Y : D) :
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {G : 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') (CategoryStruct.comp h g) = CategoryStruct.comp ((e X Y) h) (G.map g)) (X : C) :
                                                                                                  (adjunctionOfEquivLeft e he).unit.app X = (e X (F_obj X)) (CategoryStruct.id (F_obj X))
                                                                                                  def CategoryTheory.Adjunction.rightAdjointOfEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = 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
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((e X Y) g)) {Y Y' : D} (g : Y Y') :
                                                                                                      (rightAdjointOfEquiv e he).map g = (e (G_obj Y) Y') (CategoryStruct.comp ((e (G_obj Y) Y).symm (CategoryStruct.id (G_obj Y))) g)
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((e X Y) g)) (a✝ : D) :
                                                                                                      (rightAdjointOfEquiv e he).obj a✝ = G_obj a✝
                                                                                                      def CategoryTheory.Adjunction.adjunctionOfEquivRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = 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.adjunctionOfEquivRight_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((e X Y) g)) (Y : D) :
                                                                                                          (adjunctionOfEquivRight e he).counit.app Y = (e (G_obj Y) Y).symm (CategoryStruct.id (G_obj Y))
                                                                                                          @[simp]
                                                                                                          theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : 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) (CategoryStruct.comp (F.map f) g) = CategoryStruct.comp f ((e X Y) g)) (X : C) :
                                                                                                          noncomputable def CategoryTheory.Adjunction.toEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), 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
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] (X : C) :
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] :
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] (X : D) :
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] (X : C) :
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] :
                                                                                                              @[simp]
                                                                                                              theorem CategoryTheory.Adjunction.toEquivalence_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F G) [∀ (X : C), IsIso (adj.unit.app X)] [∀ (Y : D), IsIso (adj.counit.app Y)] (X : 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.

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

                                                                                                              Equations
                                                                                                                Instances For

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

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

                                                                                                                  Transport being a right adjoint along a natural isomorphism.

                                                                                                                  Transport being a left adjoint along a natural isomorphism.

                                                                                                                  noncomputable def CategoryTheory.Functor.adjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor C D) [E.IsEquivalence] :
                                                                                                                  E E.inv

                                                                                                                  An equivalence E is left adjoint to its inverse.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      @[instance 10]

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

                                                                                                                      @[instance 10]

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