English
There is a bijection between morphisms l₂ ⟶ l₁ and r₁ ⟶ r₂ induced by two adjunctions, via the composition with adjunction units/counits.
Русский
Существует биекция между морфизмами l₂ ⟶ l₁ и r₁ ⟶ r₂, индуцируемая двумя дугами через единицы/ counit.
LaTeX
$$$\\mathrm{conjugateEquiv} : (l_2 \\to l_1) \\simeq (r_1 \\to r_2)$$$
Lean4
/-- The mates equivalence commutes with horizontal composition of squares. -/
theorem mateEquiv_hcomp (α : g ≫ l₂ ⟶ l₁ ≫ h) (β : h ≫ l₄ ⟶ l₃ ≫ k) :
(mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) =
rightAdjointSquare.hcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₃ adj₄ β) :=
by
simp only [mateEquiv_apply']
dsimp [leftAdjointSquare.hcomp, rightAdjointSquare.hcomp]
calc
_ =
𝟙 _ ⊗≫
r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ :=
by bicategory
_ =
𝟙 _ ⊗≫
r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ :=
by
rw [whisker_exchange, whisker_exchange]
bicategory
_ = _ := by
rw [whisker_exchange]
bicategory
