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 #

Implementation notes #

The computation of 2-morphisms in the proof is done using calc blocks. Typically, the LHS and the RHS in each step of calc are related by simple rewriting up to associators and unitors. So the proof for each step should be of the form rw [...]; coherence. In practice, our proofs look like rw [...]; simp [bicategoricalComp]; coherence. The simp is not strictly necessary, but it speeds up the proof and allow us to avoid increasing the maxHeartbeats. The speedup is probably due to reducing the length of the expression e.g. by absorbing identity maps or applying the pentagon relation. Such a hack may not be necessary if the coherence tactic is improved. One possible way would be to perform such a simplification in the preprocessing of the coherence tactic.

TODO #

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