conjugateEquiv_symm_iso — Mathlib

English

If the inverse-conjugate of a morphism between right adjoints is an isomorphism, then the original morphism is an iso.

Русский

Если обратное сопряжение морфизма между правыми состязателями является изоморфизмом, то и сам морфизм изоморфизм.

LaTeX

$$$[IsIso\\,( (conjugateEquiv adj_1 adj_2).symm \\alpha )] \\Rightarrow IsIso(\\alpha)$$$

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)⟩⟩⟩

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