inner_map_map_iff_adjoint_comp_self

English

For a continuous linear map u: H → K, the condition ⟪u x, u y⟫ = ⟪x, y⟫ for all x,y is equivalent to u† ∘ u = 1.

Русский

Для отображения u: H → K, условие ⟪u x, u y⟫ = ⟪x, y⟫ для всех x,y эквивалентно u† ∘ u = 1.

LaTeX

$$$$\forall x,y, \langle ux, uy\rangle = \langle x, y\rangle \iff u^{*} \circ u = \mathrm{id}_{H}.$$$$

Lean4

theorem inner_map_map_iff_adjoint_comp_self (u : H →L[𝕜] K) :
    (∀ x y : H, ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ adjoint u ∘L u = 1 :=
  by
  refine ⟨fun h ↦ ext fun x ↦ ?_, fun h ↦ ?_⟩
  · refine ext_inner_right 𝕜 fun y ↦ ?_
    simpa [star_eq_adjoint, adjoint_inner_left] using h x y
  · simp [← adjoint_inner_left, ← comp_apply, h]

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