feat(Analysis/Normed/Operator): star-algebra equivalences between continuous endomorphisms are isometrically inner (leanprover-community#33066)

This is the star-algebra equivalence version of [AlgEquiv.eq_linearEquivConjAlgEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.html#AlgEquiv.eq_linearEquivConjAlgEquiv) and [ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.html#ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv). So we now have a characterization of algebra, continuous algebra, and star-algebra equivalences between endomorphisms.

The proof follows the same idea as the one in leanprover-community#28972.

Author: themathqueen

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -640,10 +640,11 @@ section Unitary
 
 variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
 
-namespace ContinuousLinearMap
-
+section linearIsometryEquiv
 variable {K : Type*} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K]
 
+namespace ContinuousLinearMap
+
 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 ↦ ?_⟩
@@ -682,6 +683,36 @@ theorem inner_map_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H
 
 end ContinuousLinearMap
 
+namespace LinearIsometryEquiv
+
+open ContinuousLinearMap ContinuousLinearEquiv in
+/-- An isometric linear equivalence of two Hilbert spaces induces an equivalence of
+⋆-algebras of their endomorphisms. -/
+def conjStarAlgEquiv (e : H ≃ₗᵢ[𝕜] K) : (H →L[𝕜] H) ≃⋆ₐ[𝕜] (K →L[𝕜] K) :=
+  .ofAlgEquiv e.toContinuousLinearEquiv.conjContinuousAlgEquiv fun x ↦ by
+    simp [star_eq_adjoint, conjContinuousAlgEquiv_apply, ← toContinuousLinearEquiv_symm, comp_assoc]
+
+@[simp] lemma conjStarAlgEquiv_apply_apply (e : H ≃ₗᵢ[𝕜] K) (x : H →L[𝕜] H) (y : K) :
+    e.conjStarAlgEquiv x y = e (x (e.symm y)) := rfl
+
+theorem symm_conjStarAlgEquiv_apply_apply (e : H ≃ₗᵢ[𝕜] K) (f : K →L[𝕜] K) (x : H) :
+    e.conjStarAlgEquiv.symm f x = e.symm (f (e x)) := rfl
+
+lemma conjStarAlgEquiv_apply (e : H ≃ₗᵢ[𝕜] K) (x : H →L[𝕜] H) :
+    e.conjStarAlgEquiv x = e ∘L x ∘L e.symm := rfl
+
+@[simp] lemma symm_conjStarAlgEquiv (e : H ≃ₗᵢ[𝕜] K) :
+    e.conjStarAlgEquiv.symm = e.symm.conjStarAlgEquiv := rfl
+
+@[simp] theorem conjStarAlgEquiv_refl : conjStarAlgEquiv (.refl 𝕜 H) = .refl := rfl
+
+theorem conjStarAlgEquiv_trans {G : Type*} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G]
+    [CompleteSpace G] (e : H ≃ₗᵢ[𝕜] K) (f : K ≃ₗᵢ[𝕜] G) :
+    (e.trans f).conjStarAlgEquiv = e.conjStarAlgEquiv.trans f.conjStarAlgEquiv := rfl
+
+end LinearIsometryEquiv
+end linearIsometryEquiv
+
 namespace Unitary
 
 theorem norm_map (u : unitary (H →L[𝕜] H)) (x : H) : ‖(u : H →L[𝕜] H) x‖ = ‖x‖ :=

Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean

@@ -5,18 +5,24 @@ Authors: Monica Omar
 -/
 module
 
+public import Mathlib.Analysis.InnerProductSpace.Adjoint
+public import Mathlib.Analysis.InnerProductSpace.Positive
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
 public import Mathlib.Analysis.Normed.Operator.Banach
 public import Mathlib.Topology.Algebra.Algebra.Equiv
 
+import Mathlib.Algebra.Central.Basic
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
+
 /-!
-# Continuous algebra equivalences between continuous endomorphisms are inner
+# Continuous (star-)algebra equivalences between continuous endomorphisms are (isometrically) inner
 
-This file shows that continuous algebra equivalences between continuous endomorphisms are inner.
+This file shows that continuous (star-)algebra equivalences between continuous endomorphisms are
+(isometrically) inner.
 See `Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean` for the non-continuous version.
 The proof follows the same idea as the non-continuous version.
 
-# TODO:
+### TODO:
 - when `V = W`, we can state that the group homomorphism
   `(V →L[𝕜] V)ˣ →* ((V →L[𝕜] V) ≃A[𝕜] (V →L[𝕜] V))` is surjective,
   see `Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective` for the non-continuous
@@ -79,3 +85,144 @@ public theorem ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv
       suffices T'.toLinearMap = Tₗ.symm from this ▸ T'.continuous
       simp [LinearMap.ext_iff, ← Tₗ.injective.eq_iff, T', this, hT, hd, Tₗ] }
   exact ⟨TL, fun A ↦ (ContinuousLinearMap.ext <| this A).symm⟩
+
+variable {𝕜 V W : Type*} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V]
+  [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace W]
+
+section auxiliaryDefs
+
+variable (e : V ≃L[𝕜] W) {α α' : 𝕜} (hα : α ≠ 0)
+  (hα2 : α' * α' = α⁻¹) (he : e.toContinuousLinearMap.adjoint ∘L e = α • .id 𝕜 V)
+  (he' : e ∘L e.toContinuousLinearMap.adjoint = α • .id 𝕜 W)
+include hα hα2 he he'
+
+/-- Scalar multiple of a continuous linear equivalence (given certain properties are satisfied). -/
+noncomputable abbrev auxContinuousLinearEquiv :
+    V ≃L[𝕜] W where
+  toLinearMap := (α' • e.toContinuousLinearMap).toLinearMap
+  invFun := (α' • e.toContinuousLinearMap.adjoint).toLinearMap
+  left_inv x := by
+    have := by simpa using congr($he x)
+    simp [smul_smul, hα2, this, hα, ← mul_assoc]
+  right_inv x := by
+    have := by simpa using congr($he' x)
+    simp [smul_smul, hα2, this, hα, ← mul_assoc]
+  continuous_toFun := (α' • e.toContinuousLinearMap).continuous
+  continuous_invFun := (α' • e.toContinuousLinearMap.adjoint).continuous
+
+@[simp] theorem coe_auxContinuousLinearEquiv :
+    (auxContinuousLinearEquiv e hα hα2 he he').toContinuousLinearMap =
+      α' • e.toContinuousLinearMap := rfl
+
+/-- Construct an isometry linear equivalence from a continuous linear equivalence
+and that its adjoint is a real-scalar multiple of its inverse. -/
+noncomputable abbrev auxIsometry (hαa : starRingEnd 𝕜 α' = α') :
+    V ≃ₗᵢ[𝕜] W where
+  __ := auxContinuousLinearEquiv e hα hα2 he he' |>.toLinearEquiv
+  norm_map' := by
+    rw [ContinuousLinearEquiv.coe_toLinearEquiv, ← ContinuousLinearEquiv.coe_coe,
+      norm_map_iff_adjoint_comp_self, coe_auxContinuousLinearEquiv,
+      MulActionSemiHomClass.map_smulₛₗ]
+    simp only [hαa, comp_smulₛₗ, RingHom.id_apply, smul_comp, smul_smul, hα2]
+    simp [he, smul_smul, hα, one_def]
+
+@[simp] theorem coe_auxIsometry (hαa : starRingEnd 𝕜 α' = α') :
+    (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.toContinuousLinearMap =
+      α' • e.toContinuousLinearMap := rfl
+
+@[simp] theorem coe_symm_auxIsometry (hαa : starRingEnd 𝕜 α' = α') :
+    (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.symm.toContinuousLinearMap =
+      α'⁻¹ • e.symm.toContinuousLinearMap := by
+  ext y
+  apply (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.injective
+  simp [smul_smul, inv_mul_cancel₀ (a := α') (by grind)]
+
+end auxiliaryDefs
+
+open ComplexOrder
+
+/-- The ⋆-algebra equivalence version of
+`ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv`.
+
+TODO: remove the hypothesis `Continuous f`, as star-algebra equivalences between endomorphisms are
+automatically continuous. -/
+public theorem StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv
+    (f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] (W →L[𝕜] W)) (hf : Continuous f) :
+    ∃ U : V ≃ₗᵢ[𝕜] W, f = U.conjStarAlgEquiv := by
+  -- Assume nontriviality of `V`.
+  by_cases! Subsingleton V
+  · by_cases! Subsingleton W
+    · use { toLinearEquiv := 0, norm_map' _ := by simp [Subsingleton.eq_zero] }
+      exact ext fun _ ↦ Subsingleton.allEq _ _
+    simpa using congr(f $(Subsingleton.allEq 0 1))
+  /- By `ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv`,
+    we know there exists a continuous linear equivalence `y : V ≃L[𝕜] W` such that
+    `f = y.conjAlgEquiv`.
+    Our goal will be to construct an isometry from `y`. We do this by first showing
+    `adjoint y ∘ y` is in the center of the endormorphisms, and as the algebra of endomorphisms
+    are central, `adjoint y ∘ y` is a scalar multiple of the identity. -/
+  obtain ⟨y, hy⟩ := (ContinuousAlgEquiv.mk f.toAlgEquiv hf
+    (f.toAlgEquiv.toLinearEquiv.continuous_symm hf)).eq_continuousLinearEquivConjContinuousAlgEquiv
+  have (x : V →L[𝕜] V) : adjoint (f x) = f (adjoint x) := map_star _ _ |>.symm
+  rw [ContinuousAlgEquiv.ext_iff] at hy
+  simp_rw [← StarAlgEquiv.coe_toAlgEquiv, ContinuousAlgEquiv.coe_mk f.toAlgEquiv hf _ ▸ hy,
+    conjContinuousAlgEquiv_apply,  adjoint_comp] at this
+  replace this (x : V →L[𝕜] V) : adjoint y.toContinuousLinearMap ∘L y ∘L adjoint x ∘L y.symm =
+      adjoint x ∘L adjoint y.toContinuousLinearMap := by
+    simp_rw [← this x, ← comp_assoc, ← adjoint_comp]
+    simp
+  replace this (x : V →L[𝕜] V) : Commute x (adjoint y.toContinuousLinearMap ∘L y) := by
+    simp_rw [commute_iff_eq, mul_def, ← comp_assoc, ← (adjoint_adjoint x ▸ this _), comp_assoc]
+    simp
+  -- Let `α : 𝕜` be that scalar, i.e., `adjoint y ∘ y = α • id`. This scalar is clearly real.
+  obtain ⟨α, hα⟩ := by simpa using (Subalgebra.mem_center_iff (R := 𝕜)).mpr fun _ ↦ this _
+  simp only [AlgHom.toRingHom_eq_coe, Algebra.toRingHom_ofId, Algebra.algebraMap_eq_smul_one] at hα
+  have : IsUnit (adjoint y.toContinuousLinearMap ∘L y) :=
+    isUnit_iff_exists.mpr ⟨y.symm ∘L adjoint y.symm.toContinuousLinearMap, by
+      simp [mul_def, ← comp_assoc, comp_assoc _ _ (adjoint y.toContinuousLinearMap),
+        ← adjoint_comp, one_def, comp_assoc _ y.toContinuousLinearMap]⟩
+  have hα_re : α = RCLike.re α := by
+    have := by simpa [IsSelfAdjoint, ← hα, one_def, star_eq_adjoint] using
+      (IsSelfAdjoint.one (W →L[𝕜] W)).adjoint_conj y.toContinuousLinearMap
+    rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
+      eq_comm] at this
+  --  Also, as `adjoint y ∘ y` is invertible, we get `α ≠ 0`.
+  have hα_ne_zero : α ≠ 0 := fun h ↦ by simp [h, ← hα] at this
+  -- As `adjoint y ∘ y` is positive, we then get `0 < α`.
+  have hα_nonneg : 0 ≤ α := by
+    have := hα_re.symm ▸ (nonneg_iff_isPositive _ |>.mpr
+      (hα_re ▸ hα ▸ isPositive_adjoint_comp_self y.toContinuousLinearMap))
+    rw [← LinearMap.isPositive_one.isPositive_smul_iff (E := V) (one_ne_zero' (V →ₗ[𝕜] V))]
+    exact (nonneg_iff_isPositive _).mp this
+  have hα_pos := RCLike.ofReal_pos.mp <| hα_re ▸ (lt_of_le_of_ne' hα_nonneg hα_ne_zero)
+  -- We also get `y ∘ adjoint y = α • id`.
+  have h_comp_adjoint : y.toContinuousLinearMap ∘L adjoint y.toContinuousLinearMap =
+      α • ContinuousLinearMap.id 𝕜 _ := by
+    ext x
+    simpa using congr(y (($hα ∘L y.symm.toContinuousLinearMap) x)).symm
+  -- Finally, we construct our isometry `1/√(re α) • y`.
+  set β := (((RCLike.re α : ℝ) ^ (-(1 / 2 : ℝ)) : ℝ) : 𝕜)
+  have hβ : β * β = α⁻¹ := by
+    rw [hα_re]
+    norm_num [β, ← RCLike.ofReal_mul, ← Real.rpow_add hα_pos, Real.rpow_neg_one]
+  set U := auxIsometry y hα_ne_zero hβ hα.symm h_comp_adjoint (by simp [β])
+  use U
+  have hβ₂ : β⁻¹ * β = 1 := by
+    refine inv_mul_cancel₀ ?_
+    simp only [β, ne_eq, map_eq_zero]
+    rw [Real.rpow_eq_zero hα_pos.le (by simp)]
+    exact ne_of_gt hα_pos
+  ext
+  simp [U.conjStarAlgEquiv_apply, U, smul_smul, hβ₂, ← conjContinuousAlgEquiv_apply, ← hy]
+
+/- TODO: Remove instance when we have `StarOrderedRing (V →L[𝕜] V)` since
+this then becomes an instance from `StarRingEquivClass.instOrderIsoClass`. -/
+public instance (priority := 100) {F : Type*} [EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)]
+    [NonUnitalAlgEquivClass F 𝕜 _ _] [StarHomClass F _ _] [ContinuousMapClass F _ _] :
+    OrderIsoClass F _ _ where
+  map_le_map_iff f x y := by
+    obtain ⟨U, hU⟩ := StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv
+      (StarAlgEquivClass.toStarAlgEquiv f : _ ≃⋆ₐ[𝕜] _) (map_continuous f)
+    have this a : f a = U.conjStarAlgEquiv a := by simpa using congr($hU a)
+    simp_rw [le_def, ← _root_.map_sub, ← isPositive_toLinearMap_iff, this]
+    exact LinearMap.isPositive_linearIsometryEquiv_conj_iff U

Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean

@@ -17,6 +17,8 @@ This file shows that given any algebra equivalence `f : End K V ≃ₐ[K] End K
 there exists a linear equivalence `T : V ≃ₗ[K] V` such that `f x = T ∘ₗ x ∘ₗ T.symm`.
 In other words, the map `MulSemiringAction.toAlgEquiv` from `GeneralLinearGroup K V` to
 `End K V ≃ₐ[K] End K V` is surjective.
+
+For the continuous versions, see `Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean`.
 -/
 
 open Module LinearMap LinearEquiv

Mathlib/Topology/Algebra/Algebra/Equiv.lean

@@ -97,6 +97,8 @@ instance continuousAlgEquivClass : ContinuousAlgEquivClass (A ≃A[R] B) R A B w
 
 theorem coe_apply (e : A ≃A[R] B) (a : A) : (e : A →A[R] B) a = e a := rfl
 
+@[simp] theorem coe_mk (e : A ≃ₐ[R] B) (he he') : ⇑(mk e he he') = e := rfl
+
 @[simp]
 theorem coe_coe (e : A ≃A[R] B) : ⇑(e : A →A[R] B) = e := rfl