Theorems · Theorem · category theory

CategoryTheory.Bicategory.mateEquiv_square

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : b ⟶ c} {r₂ : c ⟶ b} {l₃ : d ⟶ e} {r₃ : e ⟶ d}
  {l₄ : e ⟶ f} {r₄ : f ⟶ e} {l₅ : x ⟶ y} {r₅ : y ⟶ x} {l₆ : y ⟶ z} {r₆ : z ⟶ y}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (adj₄ : CategoryTheory.Bicategory.Adjunction l₄ r₄)
  (adj₅ : CategoryTheory.Bicategory.Adjunction l₅ r₅) (adj₆ : CategoryTheory.Bicategory.Adjunction l₆ r₆)
  (α : CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁)
  (γ : CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶ CategoryTheory.CategoryStruct.comp l₃ h₂)
  (δ : CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶ CategoryTheory.CategoryStruct.comp l₄ k₂),
  (CategoryTheory.Bicategory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆))
      (CategoryTheory.Bicategory.leftAdjointSquare.comp α β γ δ) =
    CategoryTheory.Bicategory.rightAdjointSquare.comp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₃) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₂ adj₄) β) ((CategoryTheory.Bicategory.mateEquiv adj₃ adj₅) γ)
      ((CategoryTheory.Bicategory.mateEquiv adj₄ adj₆) δ)

The mates equivalence commutes with composition of a square of squares. These results form the basis for an isomorphism of double categories to be proven later.

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory