Equivalent irreducible unitary representations are unitarily equivalent

An equivalence of continuous representations is a linear equivalence intertwining the actions; it need not respect the inner products. For irreducible unitary representations it can always be rescaled to one that does, so the two notions of equivalence coincide and nothing is lost by asking for equivalences that are isometries -- which is what the matrix coefficients need, since they are only invariant under isometric transport (LinearIsometryEquiv.matrixCoeff_congr).

The argument is Schur's lemma applied to T† ∘ T. If T intertwines π with ρ then, both representations being unitary, the adjoint T† intertwines ρ with π; hence T† ∘ T is a self-intertwiner of the irreducible π, so over an algebraically closed field it is a scalar c. Pairing with a vector shows c is a positive real, ‖T v‖ = √c ‖v‖, and T / √c is the isometry wanted.

Main statements

• ContRepresentation.exists_linearIsometryEquiv_congr_eq: an equivalence between finite-dimensional irreducible unitary continuous representations can be replaced by a linear isometry equivalence transporting one onto the other.

The mathematical argument follows Daniel Bump, Lie Groups, second edition, Chapter 2.

theorem ContRepresentation.instCompleteSpaceUnitaryEquivalenceDomain {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

theorem ContRepresentation.instCompleteSpaceUnitaryEquivalenceCodomain {𝕜 : Type u_1} {W : Type u_4} [RCLike 𝕜] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] : CompleteSpace W

theorem ContRepresentation.exists_linearIsometryEquiv_congr_eq {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (hπu : π.IsUnitary) (hρu : ρ.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) (φ : π.Equiv ρ) : ∃ (e : V ≃ₗᵢ[𝕜] W), (↑e).congr π = ρ

Equivalent irreducible unitary representations are unitarily equivalent. An equivalence φ of continuous representations is only a linear equivalence; rescaling it by the square root of the scalar Schur's lemma extracts from φ† ∘ φ makes it an isometry, which then transports π onto ρ in the sense of ContinuousLinearEquiv.congr.