Orthonormality of the characters of a compact group

The character of a finite-dimensional continuous representation of a compact group is a continuous function, hence square integrable for normalized Haar measure. This file records its image in L²(G) and proves the two orthogonality relations that make the irreducible unitary characters an orthonormal system: the normalization ∫ |χ_π|² = 1 for an irreducible unitary π, and the orthogonality ∫ conj χ_π · χ_ρ = 0 for a pair π, ρ admitting no nonzero continuous intertwiner ρ → π. Schur's lemma is what supplies that hypothesis for a pair of inequivalent irreducibles; deriving it is not done here.

Both statements are read off the Schur orthogonality relations of TauCeti/RepresentationTheory/Compact/SchurOrthogonality.lean and TauCeti/RepresentationTheory/Compact/Intertwiner/Basic.lean: a character is, up to conjugation, the sum of the diagonal matrix coefficients in an orthonormal basis, so an inner product of characters is a double sum of inner products of matrix coefficients. The [Finite G] shadow of these two results is Mathlib's Representation.char_orthonormal, whose finite average is replaced here by the Haar integral.

Main definitions

• ContRepresentation.characterLp: the character as an element of Lp 𝕜 2 (haarProb G).

Main statements

• ContRepresentation.inner_characterLp_eq_sum: the L² inner product of two characters is the double sum of the inner products of the diagonal matrix coefficients.
• ContRepresentation.character_orthonormal_self: first character orthogonality. The character of a finite-dimensional irreducible unitary representation is a unit vector of L²(G).
• ContRepresentation.character_orthonormal_distinct: second character orthogonality. The characters of two representations with no nonzero intertwiner between them are L²-orthogonal.

Implementation notes

The diagonal matrix coefficient matrixCoeff π hπ eᵢ eᵢ is g ↦ ⟪π g eᵢ, eᵢ⟫, while the diagonal entry of the matrix of π g that the trace sums is ⟪eᵢ, π g eᵢ⟫; in Mathlib's convention, where the inner product is conjugate linear in its first argument, these are conjugate to one another. So a character is the conjugate, not the sum, of its diagonal matrix coefficients (ContRepresentation.star_character), and inner_characterLp_eq_sum carries that conjugation as a transposition of the two arguments of the inner product. That transposition is also why character_orthonormal_distinct asks for the vanishing of the intertwiners ρ → π rather than π → ρ, and asks unitarity of π rather than of ρ: those are exactly the hypotheses of ContRepresentation.schur_orthogonality_distinct at the transposed pair. The reverse orientation is the conjugate statement, since ⟪χ_π, χ_ρ⟫ = conj ⟪χ_ρ, χ_π⟫.

Packaging the character in L² asks nothing of V beyond the finite-dimensional normed structure that the character itself needs, so characterLp is stated there; V carries an inner product only from inner_characterLp_eq_sum on, where an orthonormal basis enters. The scalars stay RCLike even for that packaging: ContinuousMap.toLp needs SecondCountableTopologyEither G 𝕜, which a general complete nontrivially normed field does not supply.

Class-function completeness is proved using Peter-Weyl in TauCeti/RepresentationTheory/Compact/Character/Basis.lean. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.characterLp {𝕜 : 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] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ↥(MeasureTheory.Lp 𝕜 2 (TauCeti.haarProb G))

The character of a finite-dimensional continuous representation as an element of L²(G) for normalized Haar measure.

The character is continuous and G is compact, so ContinuousMap.toLp applies; the normalization of Haar measure to a probability measure is what makes ‖characterLp π hπ‖ = 1 the right form of orthonormality.

Equations

• π.characterLp hπ = (ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜) (π.character hπ)

theorem ContRepresentation.characterLp_def {𝕜 : 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] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.characterLp hπ = (ContinuousMap.toLp 2 (TauCeti.haarProb G) 𝕜) (π.character hπ)

theorem ContRepresentation.coeFn_characterLp {𝕜 : 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] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ↑↑(π.characterLp hπ) =ᵐ[TauCeti.haarProb G] fun (g : G) => (LinearMap.trace 𝕜 V) ↑(π g)

A character in L² is represented, almost everywhere, by the trace of the action.

theorem ContRepresentation.inner_characterLp_eq_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) {ι : Type u_5} {κ : Type u_6} [Fintype ι] [Fintype κ] (e : OrthonormalBasis ι 𝕜 V) (f : OrthonormalBasis κ 𝕜 W) : inner 𝕜 (π.characterLp hπ) (ρ.characterLp hρ) = ∑ i : ι, ∑ k : κ, inner 𝕜 (ρ.matrixCoeffLp hρ (f k) (f k)) (π.matrixCoeffLp hπ (e i) (e i))

The L² inner product of two characters is a double sum of inner products of diagonal matrix coefficients. The two arguments are transposed on the right-hand side because a character is the conjugate of the sum of its diagonal matrix coefficients (ContRepresentation.star_character).

This is the identity through which both orthogonality relations below are read off the Schur orthogonality relations for matrix coefficients.

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

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

theorem ContRepresentation.character_orthonormal_self {𝕜 : 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] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) [IsAlgClosed 𝕜] (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) : inner 𝕜 (π.characterLp hπ) (π.characterLp hπ) = 1

First character orthogonality. The character of a finite-dimensional irreducible unitary representation of a compact group has L² inner product 1 with itself.

Summing the first Schur orthogonality relation over the diagonal collapses the d² terms of inner_characterLp_eq_sum to the d terms d⁻¹, whose sum is 1. The [Finite G] shadow of this statement is the diagonal half of Mathlib's Representation.char_orthonormal.

theorem ContRepresentation.character_orthonormal_distinct {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (hunitary : π.IsUnitary) (hdistinct : ∀ (f : ContIntertwiningMap ρ π), f.toContinuousLinearMap = 0) : inner 𝕜 (π.characterLp hπ) (ρ.characterLp hρ) = 0

Second character orthogonality. If there is no nonzero continuous intertwiner ρ → π, the characters of π and ρ are orthogonal in L²(G).

Schur's lemma is not invoked here; it is what supplies the hypothesis for a pair of inequivalent irreducibles. Unitarity is asked of π alone, and the intertwiners are those ρ → π, because inner_characterLp_eq_sum transposes the two arguments; see the module docstring.

theorem ContRepresentation.norm_characterLp_eq_one {𝕜 : 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] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) [IsAlgClosed 𝕜] (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) : ‖π.characterLp hπ‖ = 1

The character of a finite-dimensional irreducible unitary representation is a unit vector of L²(G). This is character_orthonormal_self in norm form; it is the normalization that makes the irreducible characters an orthonormal system rather than merely an orthogonal one.