Theorems · Definition · category theory

CategoryTheory.Bicategory.mateEquiv

{B : Type u} →
  [inst : CategoryTheory.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} →
                  CategoryTheory.Bicategory.Adjunction l₁ r₁ →
                    CategoryTheory.Bicategory.Adjunction l₂ r₂ →
                      (CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) ≃
                        (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.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 2-morphisms 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 2-morphisms is an iso, it does not imply the other is an iso.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

24 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Bicategory