English
Let l1 ⊣ r1 and l2 ⊣ r2 be adjunctions in a bicategory. For any α: r1 ⟶ r2, the conjugate of α under adj1 and adj2, taken via the inverse of the conjugation equivalence, is given by a specific composite: (conjugateEquiv adj1 adj2).symm α = (λ_l2)^{-1} ≫ (mateEquiv adj1 adj2).symm ((ρ_r1).hom ≫ α ≫ (λ_r2)^{-1}) ≫ (ρ_l1).hom.
Русский
Пусть в биоклассах есть две сопряжённости l1 ⊣ r1 и l2 ⊣ r2 между одинаковыми объектами. Для любого α: r1 ⟶ r2 сопряжение α через adj1 и adj2 эквивалентно определённой композиции: (conjugateEquiv adj1 adj2).symm α = (λ_l2)^{-1} ≫ (mateEquiv adj1 adj2).symm ((ρ_r1).hom ≫ α ≫ (λ_r2)^{-1}) ≫ (ρ_l1).hom.
LaTeX
$$$$(conjugateEquiv\\ adj_1\\ adj_2)\\!^{-1}(\\alpha) = (\\lambda_{l_2})^{-1} \\,\\circ\\, (\\text{mateEquiv }\\ adj_1\\ adj_2)^{-1}\\big((\\rho_{r_1})^{\\mathrm{hom}}\\circ\\alpha\\circ(\\lambda_{r_2})^{-1}\\big)\\circ (\\rho_{l_1})^{\\mathrm{hom}}.$$$$
Lean4
theorem conjugateEquiv_symm_apply (α : r₁ ⟶ r₂) :
(conjugateEquiv adj₁ adj₂).symm α =
(λ_ l₂).inv ≫ (mateEquiv adj₁ adj₂).symm ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ≫ (ρ_ l₁).hom :=
rfl
