English
If α is a natural transformation between left adjoints and its conjugate natural transformation is an isomorphism, then α itself is an isomorphism. The converse is in conjugateEquiv_symm_iso.
Русский
Пусть α — натуральное преобразование между левыми сопряжёнными; если его конюгированное преобразование является изоморфизмом, то само α также изоморфно. Обратное следует из conjugateEquiv_symm_iso.
LaTeX
$$$\\text{If } \\alpha: l_2 \\to l_1 \\text{ and } \\mathrm{conjugateEquiv}_{adj_1, adj_2}(\\alpha) \\text{ is an isomorphism, then } \\alpha \\text{ is an isomorphism.}$$$
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 only [Equiv.symm_apply_apply] using this
infer_instance
