English
Let adj1 and adj2 be adjunctions in a bicategory. If α is an isomorphism between the right adjoints r1 and r2, then its conjugate under the conjugate equivalence (conjugateEquiv adj1 adj2) is an isomorphism.
Русский
Пусть существую взаимно вложенные соответствия adj1 и adj2 в двимерном категории. Если α является изоморфизмом между правыми сопряжёнными r1 и r2, то его конюгированное отображение через сопряжённое отображение (conjugateEquiv adj1 adj2) также является изоморфизмом.
LaTeX
$$$\\IsIso\\big((\\mathrm{conjugateEquiv}\\; adj_1\\ adj_2)\\mathrm{symm}\\,\\alpha\\big)$$$
Lean4
/-- If `α` is an isomorphism between right adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_symm_of_iso`.
-/
instance conjugateEquiv_symm_iso (α : r₁ ⟶ r₂) [IsIso α] : IsIso ((conjugateEquiv adj₁ adj₂).symm α) :=
⟨⟨(conjugateEquiv adj₂ adj₁).symm (inv α),
⟨conjugateEquiv_symm_comm _ _ (by simp), conjugateEquiv_symm_comm _ _ (by simp)⟩⟩⟩
