English
In a bicategory with adjunctions adj1: l1 ⊣ r1 and adj2: l2 ⊣ r2, and α: r1 ⟶ r2, the symmetrically conjugate of α via adj1 and adj2' equals a certain explicit expression involving unit and counit data, whiskering, and associators. The result matches the previous conjugateSymm_apply after rewriting with mate equivalences.
Русский
В бикатегории с сопряжённостями adj1 и adj2' и стрелкой α между правыми сопряжёнными, симметрично сопряжённое α выражается через единицы/коуниты и композиции, согласованно со стандартными преобразованиями.
LaTeX
$$$$ (conjugateEquiv\\ adj_1\\ adj_2).\\text{symm}(\\alpha) = (\\lambda\\_{}).inv \\;\\circ\\; adj_1.\\text{unit} \\;\\triangleright\\; l_2 \\;\\circ\\; (\\alpha\\_{}\\_\\_\\_).hom \\;\\circ\\; l_1 \\triangleleft\\; \\alpha \\triangleright l_2 \\circ\\ adj_2.counit \\circ (\\rho_\\_).hom $$$$
Lean4
theorem conjugateEquiv_symm_apply' (α : r₁ ⟶ r₂) :
(conjugateEquiv adj₁ adj₂).symm α =
(λ_ _).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ _ _ _).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ _).hom :=
by
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']
bicategory
