Continuous (star-)algebra equivalences between continuous endomorphisms are (isometrically) 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:

• 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 version of this.

theorem ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [SeparatingDual 𝕜 V] [SeparatingDual 𝕜 W] (f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W) : ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

This is the continuous version of AlgEquiv.eq_linearEquivConjAlgEquiv.

theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [SeparatingDual 𝕜 V] [SeparatingDual 𝕜 W] : Function.Surjective conjContinuousAlgEquiv

theorem StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace W] (f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W) (hf : Continuous ⇑f) : ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

The ⋆-algebra equivalence version of ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv.

TODO: remove the hypothesis Continuous f, as star-algebra equivalences between endomorphisms are automatically continuous.

@[instance 100]

instance instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [CompleteSpace W] {F : Type u_4} [EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)] [NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)] [StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)] [ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)] : OrderIsoClass F (V →L[𝕜] V) (W →L[𝕜] W)