Theorems · Theorem · category theory

CategoryTheory.iterated_mateEquiv_conjugateEquiv

∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F₁ : CategoryTheory.Functor A C} {U₁ : CategoryTheory.Functor C A}
  {F₂ : CategoryTheory.Functor B D} {U₂ : CategoryTheory.Functor D B} {L₁ : CategoryTheory.Functor A B}
  {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor C D} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : F₁ ⊣ U₁) (adj₄ : F₂ ⊣ U₂) (α : CategoryTheory.TwoSquare F₁ L₁ L₂ F₂),
  ((CategoryTheory.mateEquiv adj₄ adj₃) ((CategoryTheory.mateEquiv adj₁ adj₂) α)).natTrans =
    (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

When all four functors in a square are left adjoints, the mates operation can be iterated: `` L₁ R₁ R₁ C --→ D C ←-- D C ←-- D F₁ ↓ ↗ ↓ F₂ F₁ ↓ ↘ ↓ F₂ U₁ ↑ ↙ ↑ U₂ E --→ F E ←-- F E ←-- F L₂ R₂ R₂ `` In this case the iterated mate equals the conjugate of the original transformation and is thus an isomorphism if and only if the original transformation is. This explains why some Beck-Chevalley natural transformations are natural isomorphisms.

Defined in

Mathlib.CategoryTheory.Adjunction.Mates

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category