adjoint_eq_symm — Mathlib

English

If e is a linear isometry between inner product spaces H and K, then the adjoint of the associated bounded linear map equals the inverse of e. In symbols, adjoint(e) = e.symm = e^{-1}.

Русский

Пусть e — линейная изометрия между пространствами H и K. Тогда сопряжённый к e оператор равен обратному линейному отображению e: adjoint(e) = e^{-1}.

LaTeX

$$$\operatorname{adjoint}(e) = e^{-1}$$$

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.adjoint_eq_symm (e : H ≃ₗᵢ[𝕜] K) : adjoint (e : H →L[𝕜] K) = e.symm :=
  let e' := (e : H →L[𝕜] K)
  calc
    adjoint e' = adjoint e' ∘L (e' ∘L e.symm) :=
      by
      convert (adjoint e').comp_id.symm
      ext
      simp [e']
    _ = e.symm := by
      rw [← comp_assoc, norm_map_iff_adjoint_comp_self e' |>.mp e.norm_map]
      exact (e.symm : K →L[𝕜] H).id_comp

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