feat: unitary operators on a Hilbert space coincide with linear isome…

…tric equivalences (#10858)

This constructs a group isomorphism `unitary (H →L[𝕜] H) ≃⋆ (H ≃ₗᵢ[𝕜] H)` where `H` is a Hilbert space. In addition, several lemmas are provided for convenience concerning unitary operators.

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -506,6 +506,99 @@ theorem im_inner_adjoint_mul_self_eq_zero (T : E →ₗ[𝕜] E) (x : E) :
 
 end LinearMap
 
+section Unitary
+
+variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
+
+namespace ContinuousLinearMap
+
+variable {K : Type*} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K]
+
+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]
+
+theorem norm_map_iff_adjoint_comp_self (u : H →L[𝕜] K) :
+    (∀ x : H, ‖u x‖ = ‖x‖) ↔ adjoint u ∘L u = 1 := by
+  rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_map_iff_adjoint_comp_self]
+
+@[simp]
+lemma _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
+
+@[simp]
+lemma _root_.LinearIsometryEquiv.star_eq_symm (e : H ≃ₗᵢ[𝕜] H) :
+    star (e : H →L[𝕜] H) = e.symm :=
+  e.adjoint_eq_symm
+
+theorem norm_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H) :
+    ‖u x‖ = ‖x‖ :=
+  u.norm_map_iff_adjoint_comp_self.mpr (unitary.star_mul_self_of_mem hu) x
+
+theorem inner_map_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x y : H) :
+    ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜 :=
+  u.inner_map_map_iff_adjoint_comp_self.mpr (unitary.star_mul_self_of_mem hu) x y
+
+end ContinuousLinearMap
+
+namespace unitary
+
+theorem norm_map (u : unitary (H →L[𝕜] H)) (x : H) : ‖(u : H →L[𝕜] H) x‖ = ‖x‖ :=
+  u.val.norm_map_of_mem_unitary u.property x
+
+theorem inner_map_map (u : unitary (H →L[𝕜] H)) (x y : H) :
+    ⟪(u : H →L[𝕜] H) x, (u : H →L[𝕜] H) y⟫_𝕜 = ⟪x, y⟫_𝕜 :=
+  u.val.inner_map_map_of_mem_unitary u.property x y
+
+/-- The unitary elements of continuous linear maps on a Hilbert space coincide with the linear
+isometric equivalences on that Hilbert space. -/
+noncomputable def linearIsometryEquiv : unitary (H →L[𝕜] H) ≃* (H ≃ₗᵢ[𝕜] H) where
+  toFun u :=
+    { (u : H →L[𝕜] H) with
+      norm_map' := norm_map u
+      invFun := ↑(star u)
+      left_inv := fun x ↦ congr($(star_mul_self u).val x)
+      right_inv := fun x ↦ congr($(mul_star_self u).val x) }
+  invFun e :=
+    { val := e
+      property := by
+        let e' : (H →L[𝕜] H)ˣ :=
+          { val := (e : H →L[𝕜] H)
+            inv := (e.symm : H →L[𝕜] H)
+            val_inv := by ext; simp
+            inv_val := by ext; simp }
+        exact IsUnit.mem_unitary_of_star_mul_self ⟨e', rfl⟩ <|
+          (e : H →L[𝕜] H).norm_map_iff_adjoint_comp_self.mp e.norm_map }
+  left_inv u := Subtype.ext rfl
+  right_inv e := LinearIsometryEquiv.ext fun x ↦ rfl
+  map_mul' u v := by ext; rfl
+
+@[simp]
+lemma linearIsometryEquiv_coe_apply (u : unitary (H →L[𝕜] H)) :
+    linearIsometryEquiv u = (u : H →L[𝕜] H) :=
+  rfl
+
+@[simp]
+lemma linearIsometryEquiv_coe_symm_apply (e : H ≃ₗᵢ[𝕜] H) :
+    linearIsometryEquiv.symm e = (e : H →L[𝕜] H) :=
+  rfl
+
+end unitary
+
+end Unitary
+
 section Matrix
 
 open Matrix LinearMap

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -1305,6 +1305,12 @@ theorem LinearEquiv.isometryOfInner_toLinearEquiv (f : E ≃ₗ[𝕜] E') (h) :
   rfl
 #align linear_equiv.isometry_of_inner_to_linear_equiv LinearEquiv.isometryOfInner_toLinearEquiv
 
+/-- A linear map is an isometry if and it preserves the inner product. -/
+theorem LinearMap.norm_map_iff_inner_map_map {F : Type*} [FunLike F E E'] [LinearMapClass F 𝕜 E E']
+    (f : F) : (∀ x, ‖f x‖ = ‖x‖) ↔ (∀ x y, ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) :=
+  ⟨({ toLinearMap := LinearMapClass.linearMap f, norm_map' := · : E →ₗᵢ[𝕜] E' }.inner_map_map),
+    (LinearMapClass.linearMap f |>.isometryOfInner · |>.norm_map)⟩
+
 /-- A linear isometry preserves the property of being orthonormal. -/
 theorem LinearIsometry.orthonormal_comp_iff {v : ι → E} (f : E →ₗᵢ[𝕜] E') :
     Orthonormal 𝕜 (f ∘ v) ↔ Orthonormal 𝕜 v := by