conjugateEquiv_iso — Mathlib

English

If the conjugate of a left-adjoint morphism is an isomorphism, then the original morphism is an isomorphism.

Русский

Если конъюгат левого сопряжения изоморфизм, то и исходный морфизм является изоморфизмом.

LaTeX

$$$\\text{IsIso}(\\text{conjugateEquiv } adj_1 adj_2 \\alpha) \\Rightarrow \\text{IsIso}(\\alpha)$$$

Lean4

/-- If `α` is an isomorphism between left adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_of_iso`.
-/
instance conjugateEquiv_iso (α : L₂ ⟶ L₁) [IsIso α] : IsIso (conjugateEquiv adj₁ adj₂ α) :=
  ⟨⟨conjugateEquiv adj₂ adj₁ (inv α), ⟨conjugateEquiv_comm _ _ (by simp), conjugateEquiv_comm _ _ (by simp)⟩⟩⟩

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