Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction

Adjunctions in bicategories #

For 1-morphisms f : a ⟶ b and g : b ⟶ a in a bicategory, an adjunction between f and g consists of a pair of 2-morphism η : 𝟙 a ⟶ f ≫ g and ε : g ≫ f ⟶ 𝟙 b satisfying the triangle identities. The 2-morphism η is called the unit and ε is called the counit.

Main definitions #

TODO #

@[reducible, inline]

The 2-morphism defined by the following pasting diagram:

a ------ ▸ a
  \    η      ◥   \
  f \   g  /       \ f
       ◢  /     ε      ◢
        b ------ ▸ b
Equations
Instances For
    @[reducible, inline]

    The 2-morphism defined by the following pasting diagram:

            a ------ ▸ a
           ◥  \     η      ◥
      g /      \ f     / g
      /    ε      ◢   /
    b ------ ▸ b
    
    Equations
    Instances For
      structure CategoryTheory.Bicategory.Adjunction {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a b) (g : b a) :

      Adjunction between two 1-morphisms.

      Instances For
        @[simp]

        The composition of the unit and the counit is equal to the identity up to unitors.

        @[simp]

        The composition of the unit and the counit is equal to the identity up to unitors.

        Adjunction between two 1-morphisms.

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

          Adjunction between identities.

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

            Auxiliary definition for adjunction.comp.

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

              Auxiliary definition for adjunction.comp.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Bicategory.Adjunction.comp_counit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) :
                (adj₁.comp adj₂).counit = adj₁.compCounit adj₂
                @[simp]
                theorem CategoryTheory.Bicategory.Adjunction.comp_unit {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f₁ : a b} {g₁ : b a} {f₂ : b c} {g₂ : c b} (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂) :
                (adj₁.comp adj₂).unit = adj₁.compUnit adj₂

                Composition of adjunctions.

                Equations
                • adj₁.comp adj₂ = { unit := adj₁.compUnit adj₂, counit := adj₁.compCounit adj₂, left_triangle := , right_triangle := }
                Instances For

                  An auxiliary definition for mkOfAdjointifyCounit.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    structure CategoryTheory.Bicategory.Equivalence {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) :
                    Type (max v w)

                    Adjoint equivalences between two objects.

                    Instances For

                      The composition of the unit and the counit is equal to the identity up to unitors.

                      Adjoint equivalences between two objects.

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

                        The identity 1-morphism is an equivalence.

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

                          Construct an adjoint equivalence from 2-isomorphisms by upgrading ε to a counit.

                          Equations
                          Instances For
                            structure CategoryTheory.Bicategory.RightAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (left : a b) :
                            Type (max v w)

                            A structure giving a chosen right adjoint of a 1-morphism left.

                            Instances For
                              class CategoryTheory.Bicategory.IsLeftAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (left : a b) :

                              The existence of a right adjoint of f.

                              Instances

                                Use the axiom of choice to extract a right adjoint from an IsLeftAdjoint instance.

                                Equations
                                Instances For
                                  structure CategoryTheory.Bicategory.LeftAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (right : b a) :
                                  Type (max v w)

                                  A structure giving a chosen left adjoint of a 1-morphism right.

                                  Instances For
                                    class CategoryTheory.Bicategory.IsRightAdjoint {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (right : b a) :

                                    The existence of a left adjoint of f.

                                    Instances

                                      Use the axiom of choice to extract a left adjoint from an IsRightAdjoint instance.

                                      Equations
                                      Instances For