Theorems · Definition · category theory

CategoryTheory.Bicategory.conjugateEquiv

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {c d : B} →
      {l₁ l₂ : c ⟶ d} →
        {r₁ r₂ : d ⟶ c} →
          CategoryTheory.Bicategory.Adjunction l₁ r₁ →
            CategoryTheory.Bicategory.Adjunction l₂ r₂ → (l₂ ⟶ l₁) ≃ (r₁ ⟶ r₂)

Given two adjunctions l₁ ⊣ r₁ and l₂ ⊣ r₂ both between objects c, d, there is a bijection between 2-morphisms l₂ ⟶ l₁ and 2-morphisms r₁ ⟶ r₂. This is defined as a special case of mateEquiv, where the two "vertical" 1-morphisms are identities. This bijection is conjugateEquiv; the image of a 2-morphism under it is called its conjugate. Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a 2-morphism is an iso iff its image under the bijection is an iso.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

41 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory