Theorems · Theorem · category theory

CategoryTheory.conjugateEquiv_associator_hom

∀ {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] {L₀₁ : CategoryTheory.Functor A B} {R₁₀ : CategoryTheory.Functor B A}
  {L₁₂ : CategoryTheory.Functor B C} {R₂₁ : CategoryTheory.Functor C B} {L₂₃ : CategoryTheory.Functor C D}
  {R₃₂ : CategoryTheory.Functor D C} (adj₀₁ : L₀₁ ⊣ R₁₀) (adj₁₂ : L₁₂ ⊣ R₂₁) (adj₂₃ : L₂₃ ⊣ R₃₂),
  (CategoryTheory.conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃))
      (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom

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