The unitary model of a finite-dimensional representation of a compact group

Weyl's unitarian trick, in TauCeti/RepresentationTheory/Compact/Unitarizable.lean, averages the inner product of a continuous representation π of a compact group over Haar measure and records the averaged form through its Gram operator S, a positive-definite self-adjoint operator with (π g)† ∘ S ∘ (π g) = S. That is an invariant form, not yet a unitary representation: Lean fixes one InnerProductSpace structure on the carrier, and π is in general not unitary for it.

This file closes the gap in finite dimensions. Changing coordinates by the automorphism A that standardizes the invariant form (TauCeti.exists_continuousLinearEquiv_inner_map_map, morally A = S ^ (-1 / 2)) conjugates π into a representation that is unitary for the given inner product:

ContRepresentation.exists_isUnitary_congr produces e : V ≃L[𝕜] V with IsUnitary (congr e π).

What this buys is a replacement of π by an equivalent representation, not by π itself, so a property may be proved for unitary representations alone exactly when it is invariant under conjugation by a continuous linear automorphism. The two consequences recorded here are the form that fact is consumed in, and both are of that kind: a matrix coefficient of an arbitrary finite-dimensional continuous representation is a matrix coefficient of a unitary one, and hence the representative ring 𝓡(G) is spanned by the matrix coefficients of the unitary finite-dimensional continuous representations alone.

Main statements

• ContRepresentation.exists_isUnitary_congr: a finite-dimensional continuous representation of a compact group is conjugate to a unitary one.
• ContRepresentation.exists_isUnitary_matrixCoeff_eq: its matrix coefficients are matrix coefficients of a unitary representation.
• TauCeti.isRepresentative_iff_exists_isUnitary: a representative function is a matrix coefficient of a unitary representation on a standard model.

Implementation notes

The conjugating automorphism is not asked to be canonical: TauCeti.exists_continuousLinearEquiv_inner_map_map chooses an eigenbasis of the Gram operator, and only its existence is exported. Nothing downstream needs more, since the unitary structure it produces is unique up to a unitary equivalence anyway.

Finite dimensionality enters only through that standardization, which is proved by the spectral theorem; the Gram operator itself is built for an arbitrary Hilbert-space carrier.

Unitarization allows the matrix coefficients of arbitrary representations to be expanded in those of unitary irreducible representations. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

theorem ContRepresentation.exists_isUnitary_congr {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ∃ (e : V ≃L[𝕜] V), (e.congr π).IsUnitary

A finite-dimensional continuous representation of a compact group is conjugate to a unitary one. There is a continuous linear automorphism e of the carrier for which the transported representation ContinuousLinearEquiv.congr e π preserves the inner product.

This is the unitarian trick in its usable form. Haar averaging supplies the invariant positive-definite form ⟪S ·, ·⟫; the automorphism A carrying the standard inner product to that form (TauCeti.exists_continuousLinearEquiv_inner_map_map) conjugates the invariance of the form into unitarity of A⁻¹ ∘ π · ∘ A.

theorem ContRepresentation.exists_isUnitary_matrixCoeff_eq {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ∃ (ρ : ContRepresentation 𝕜 G V) (hρ : Continuous ⇑ρ), ρ.IsUnitary ∧ ∃ (v' : V) (w' : V), π.matrixCoeff hπ v w = ρ.matrixCoeff hρ v' w'

A matrix coefficient of a finite-dimensional continuous representation of a compact group is a matrix coefficient of a unitary one, on the same carrier and at suitably moved vectors.

Matrix coefficients depend only on the equivalence class of a representation (ContinuousLinearEquiv.matrixCoeff_congr_adjoint), so the conjugate unitary model produced by ContRepresentation.exists_isUnitary_congr produces every matrix coefficient of the original.

theorem TauCeti.isRepresentative_iff_exists_isUnitary {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {f : C(G, 𝕜)} : IsRepresentative f ↔ ∃ (n : ℕ) (π : ContRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin n))) (hπ : Continuous ⇑π), π.IsUnitary ∧ ∃ (v : EuclideanSpace 𝕜 (Fin n)) (w : EuclideanSpace 𝕜 (Fin n)), f = π.matrixCoeff hπ v w

The representative functions of a compact group are the matrix coefficients of its unitary finite-dimensional continuous representations. Restricting the representations allowed in the definition of TauCeti.IsRepresentative to the unitary ones changes nothing.

The forward direction is unitarization; the reverse is the definition. Consequently the representative ring 𝓡(G), whose uniform density in C(G, 𝕜) is the analytic core of the Peter-Weyl theorem, is spanned by the matrix coefficients of unitary representations, which are the ones Schur orthogonality applies to.