English
Iterating the mates construction corresponds to conjugating the original morphism by the horizontal/vertical compositions of adjunctions.
Русский
Итерирование конструкции mateEquiv соответствует сопряжению исходного преобразования композициями сопряжений по горизонтали/вертикали.
LaTeX
$$$\\text{mateEquiv }(adj_4, adj_3)(\\text{mateEquiv }(adj_1, adj_2) α) = \\text{conjugateEquiv}(adj_1\\.comp\\, adj_4, adj_3\\.comp\\, adj_2) α$$$
Lean4
/-- If `α` is a natural transformation between right adjoints whose conjugate natural transformation is
an isomorphism, then `α` is an isomorphism. The converse is given in `conjugateEquiv_symm_iso`.
-/
theorem conjugateEquiv_symm_of_iso (α : R₁ ⟶ R₂) [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] : IsIso α :=
by
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α)) by simpa using this
infer_instance
