Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Mates in bicategories #

This file establishes the bijection between the 2-cells

         l₁                  r₁
      c --→ d             c ←-- d
    g ↓  ↗  ↓ h         g ↓  ↘  ↓ h
      e --→ f             e ←-- f
         l₂                  r₂

where l₁ ⊣ r₁ and l₂ ⊣ r₂. The corresponding natural transformations are called mates.

For the bicategory Cat, the definitions in this file are provided in Mathlib/CategoryTheory/Adjunction/Mates.lean, where you can find more detailed documentation about mates.

Remarks #

To be precise, the definitions in Mathlib/CategoryTheory/Adjunction/Mates.lean are universe polymorphic, so they are not simple specializations of the definitions in this file.

source
def CategoryTheory.Bicategory.mateEquiv {B : Type u} [Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c} {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : Adjunction l₁ r₁) (adj₂ : Adjunction l₂ r₂) :
(CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h) ≃ (CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂)

Suppose we have a square of 1-morphisms (where the top and bottom are adjunctions l₁ ⊣ r₁ and l₂ ⊣ r₂ respectively).

  c ↔ d
g ↓   ↓ h
  e ↔ f

Then we have a bijection between natural transformations g ≫ l₂ ⟶ l₁ ≫ h and r₁ ≫ g ⟶ h ≫ r₂. This can be seen as a bijection of the 2-cells:

     l₁                  r₁
  c --→ d             c ←-- d
g ↓  ↗  ↓ h         g ↓  ↘  ↓ h
  e --→ f             e ←-- f
     L₂                  R₂

Note that if one of the transformations is an iso, it does not imply the other is an iso.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Bicategory.mateEquiv_symm_apply {B : Type u} [Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c} {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : Adjunction l₁ r₁) (adj₂ : Adjunction l₂ r₂) (β : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂) :
    (mateEquiv adj₁ adj₂).symm β = bicategoricalComp (CategoryStruct.id (CategoryStruct.comp g l₂)) (bicategoricalComp (whiskerRight (whiskerRight adj₁.unit g) l₂) (bicategoricalComp (whiskerLeft l₁ (whiskerRight β l₂)) (bicategoricalComp (whiskerLeft l₁ (whiskerLeft h adj₂.counit)) (CategoryStruct.id (CategoryStruct.comp l₁ h)))))
    source
    @[simp]
    theorem CategoryTheory.Bicategory.mateEquiv_apply {B : Type u} [Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c} {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : Adjunction l₁ r₁) (adj₂ : Adjunction l₂ r₂) (α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h) :
    (mateEquiv adj₁ adj₂) α = bicategoricalComp (CategoryStruct.id (CategoryStruct.comp r₁ g)) (bicategoricalComp (whiskerLeft r₁ (whiskerLeft g adj₂.unit)) (bicategoricalComp (whiskerLeft r₁ (whiskerRight α r₂)) (bicategoricalComp (whiskerRight (whiskerRight adj₁.counit h) r₂) (CategoryStruct.id (CategoryStruct.comp h r₂)))))
    source
    def CategoryTheory.Bicategory.leftAdjointSquare.vcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d} {h₂ : d ⟶ f} {l₁ : a ⟶ b} {l₂ : c ⟶ d} {l₃ : e ⟶ f} (α : CategoryStruct.comp g₁ l₂ ⟶ CategoryStruct.comp l₁ h₁) (β : CategoryStruct.comp g₂ l₃ ⟶ CategoryStruct.comp l₂ h₂) :
    CategoryStruct.comp (CategoryStruct.comp g₁ g₂) l₃ ⟶ CategoryStruct.comp l₁ (CategoryStruct.comp h₁ h₂)

    Squares between left adjoints can be composed "vertically" by pasting.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Bicategory.rightAdjointSquare.vcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d} {h₂ : d ⟶ f} {r₁ : b ⟶ a} {r₂ : d ⟶ c} {r₃ : f ⟶ e} (α : CategoryStruct.comp r₁ g₁ ⟶ CategoryStruct.comp h₁ r₂) (β : CategoryStruct.comp r₂ g₂ ⟶ CategoryStruct.comp h₂ r₃) :
      CategoryStruct.comp r₁ (CategoryStruct.comp g₁ g₂) ⟶ CategoryStruct.comp (CategoryStruct.comp h₁ h₂) r₃

      Squares between right adjoints can be composed "vertically" by pasting.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CategoryTheory.Bicategory.mateEquiv_vcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d} {h₂ : d ⟶ f} {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} {l₃ : e ⟶ f} {r₃ : f ⟶ e} (adj₁ : Adjunction l₁ r₁) (adj₂ : Adjunction l₂ r₂) (adj₃ : Adjunction l₃ r₃) (α : CategoryStruct.comp g₁ l₂ ⟶ CategoryStruct.comp l₁ h₁) (β : CategoryStruct.comp g₂ l₃ ⟶ CategoryStruct.comp l₂ h₂) :
        (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α β) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)

        The mates equivalence commutes with vertical composition.

        source
        def CategoryTheory.Bicategory.leftAdjointSquare.hcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g : a ⟶ d} {h : b ⟶ e} {k : c ⟶ f} {l₁ : a ⟶ b} {l₂ : d ⟶ e} {l₃ : b ⟶ c} {l₄ : e ⟶ f} (α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h) (β : CategoryStruct.comp h l₄ ⟶ CategoryStruct.comp l₃ k) :
        CategoryStruct.comp g (CategoryStruct.comp l₂ l₄) ⟶ CategoryStruct.comp (CategoryStruct.comp l₁ l₃) k

        Squares between left adjoints can be composed "horizontally" by pasting.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def CategoryTheory.Bicategory.rightAdjointSquare.hcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g : a ⟶ d} {h : b ⟶ e} {k : c ⟶ f} {r₁ : b ⟶ a} {r₂ : e ⟶ d} {r₃ : c ⟶ b} {r₄ : f ⟶ e} (α : CategoryStruct.comp r₁ g ⟶ CategoryStruct.comp h r₂) (β : CategoryStruct.comp r₃ h ⟶ CategoryStruct.comp k r₄) :
          CategoryStruct.comp (CategoryStruct.comp r₃ r₁) g ⟶ CategoryStruct.comp k (CategoryStruct.comp r₄ r₂)

          Squares between right adjoints can be composed "horizontally" by pasting.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem CategoryTheory.Bicategory.mateEquiv_hcomp {B : Type u} [Bicategory B] {a b c d e f : B} {g : a ⟶ d} {h : b ⟶ e} {k : c ⟶ f} {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : d ⟶ e} {r₂ : e ⟶ d} {l₃ : b ⟶ c} {r₃ : c ⟶ b} {l₄ : e ⟶ f} {r₄ : f ⟶ e} (adj₁ : Adjunction l₁ r₁) (adj₂ : Adjunction l₂ r₂) (adj₃ : Adjunction l₃ r₃) (adj₄ : Adjunction l₄ r₄) (α : CategoryStruct.comp g l₂ ⟶ CategoryStruct.comp l₁ h) (β : CategoryStruct.comp h l₄ ⟶ CategoryStruct.comp l₃ k) :
            (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) = rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₃ adj₄) β)

            The mates equivalence commutes with horizontal composition of squares.