conjugateEquiv_iso — Mathlib

English

Conjugation preserves isomorphisms at the level of left adjoints in a bicategory context.

Русский

Сопряжение сохраняет изоморфизмы на уровне левых сопряжений в Bicategory контексте.

LaTeX

$$$\\text{conjugateEquiv_iso } (adj_1 adj_2) (\\alpha) : IsIso(conjugateEquiv adj_1 adj_2 α)$$$

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

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