conjugateEquiv_symm_of_iso — Mathlib

English

If α is a morphism between right adjoints whose conjugate is an isomorphism, then α is an isomorphism.

Русский

Если α — морфизм между правыми сопряжёнными, чьё сопряжение является изоморфизмом, то и само α является изоморфизмом.

LaTeX

$$$\\text{If } \\alpha: r_1 \\to r_2 \\text{ with } IsIso((\\mathrm{conjugateEquiv}\\ adj_1\\ adj_2).\\mathrm{symm}\\ \\alpha), \\text{ then } IsIso(\\alpha).$$$

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 only [Equiv.apply_symm_apply] using this
  infer_instance

Похожие утверждения