conjugateEquiv_symm_comp — Mathlib

English

If α is an isomorphism between left adjoints, then its conjugate via adjunctions is an isomorphism; converse is given in conjugateEquiv_of_iso.

Русский

Если α — изоморфизм между левого сопряжённых, то его сопряжение — изоморфизм; обратное следует из conjugateEquiv_of_iso.

LaTeX

$$$$ \\text{If } α: l_2 \\to l_1 \\text{ is an isomorphism, then } (\\conjugateEquiv adj_1 adj_2) α \\text{ is an isomorphism. } $$$$

Lean4

@[simp]
theorem conjugateEquiv_symm_comp (α : r₁ ⟶ r₂) (β : r₂ ⟶ r₃) :
    (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β) :=
  by
  rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]
  simp only [Equiv.apply_symm_apply]

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