Theorems · Theorem · category theory

CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f₁ : a ⟶ c} {u₁ : c ⟶ a} {f₂ : b ⟶ d} {u₂ : d ⟶ b}
  {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction f₁ u₁)
  (adj₄ : CategoryTheory.Bicategory.Adjunction f₂ u₂)
  (α : CategoryTheory.CategoryStruct.comp f₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ f₂),
  (CategoryTheory.Bicategory.mateEquiv adj₄ adj₃) ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α) =
    (CategoryTheory.Bicategory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

When all four morphisms in a square are left adjoints, the mates operation can be iterated: `` l₁ r₁ r₁ a --→ b a ←-- b a ←-- b f₁ ↓ ↗ ↓ f₂ f₁ ↓ ↘ ↓ f₂ u₁ ↑ ↙ ↑ u₂ c --→ d c ←-- d c ←-- d l₂ r₂ r₂ `` In this case the iterated mate equals the conjugate of the original 2-morphism and is thus an isomorphism if and only if the original 2-morphism is. This explains why some Beck-Chevalley 2-morphisms are isomorphisms.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory