English
The conjugation gives an equivalence between natural isomorphisms: given adjunctions adj1, adj2 and an isomorphism α: L2 ≅ L1, the conjugate (conjugateEquiv adj1 adj2).symm α is an isomorphism in the opposite direction, and yields an isomorphism between L1 and L2.
Русский
Сопряжение задаёт эквивалентность между естественными изоморфизмами: при наличии сопряжений adj1, adj2 и изоморфизма α: L2 ≅ L1 сопряжение (conjugateEquiv adj1 adj2).symm α даёт изоморфизм между L1 и L2.
LaTeX
$$$IsIso(EquivLike.toFunLike.coe(\\text{conjugateEquiv } adj_1 adj_2) α)$$$
Lean4
/-- If `α` is a natural transformation between left adjoints whose conjugate natural transformation
is an isomorphism, then `α` is an isomorphism. The converse is given in `Conjugate_iso`.
-/
theorem conjugateEquiv_of_iso (α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] : IsIso α :=
by
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using this
infer_instance
