The irreducible characters are a Hilbert basis of the class functions

Peter-Weyl (TauCeti/RepresentationTheory/Compact/PeterWeyl.lean) makes the normalized matrix coefficients of a skeleton of the unitary dual a Hilbert basis of L²(G). This file cuts that basis down to the closed subspace TauCeti.classFunctionLp of class functions and finds the irreducible characters there: they are a Hilbert basis of the class functions, the compact-group form of "the irreducible characters are a basis of the class functions".

The argument

Fix a finite-dimensional irreducible unitary continuous π and a class function f. The pairing A v w = ⟪(π)_{v,w}, f⟫ is linear in v and conjugate linear in w, so it is ⟪w, T v⟫ for a unique endomorphism T of the carrier. Conjugation-invariance of f says exactly that A is unchanged when both vectors are moved by π h (TauCeti.ContRepresentation.inner_matrixCoeffLp_map_map), and that makes T an intertwiner. Schur's lemma over an algebraically closed field collapses T to a scalar, so

⟪(π)_{v,w}, f⟫ = c · ⟪w, v⟫

(TauCeti.ContRepresentation.exists_forall_inner_matrixCoeffLp_eq): a class function sees only the trace direction of each Peter-Weyl block. Taking v = w over an orthonormal basis and summing identifies c · dim V with the pairing of f against the sum of the diagonal matrix coefficients, which is the conjugate of the character, not the character. Inversion g ↦ g⁻¹ exchanges the two (ContRepresentation.invLpₗᵢ_characterLp), and it is an isometry preserving the class functions, so running the argument on the inverse-translate of f is what turns orthogonality to every character into the vanishing of every Peter-Weyl coefficient.

Main definitions

• TauCeti.characterFamily: the characters of a family of models, as elements of the class functions.
• TauCeti.characterBasis: the Hilbert basis of classFunctionLp given by the irreducible characters, for a skeleton of the unitary dual.
• TauCeti.stdCharacterBasis: the same on the chosen representatives of TauCeti.IrrepClass, so that no skeleton has to be supplied.

Main statements

• TauCeti.ContRepresentation.exists_forall_inner_matrixCoeffLp_eq: against a class function, the matrix coefficients of an irreducible pair off into a single scalar.
• TauCeti.eq_zero_of_forall_inner_characterLp_eq_zero: class-function completeness. A class function orthogonal to every irreducible character is zero.
• TauCeti.coe_characterBasis, TauCeti.coe_stdCharacterBasis: the basis is the characters themselves.

References

The closed subspace of class functions and the membership of the characters in it are developed in TauCeti/RepresentationTheory/Compact/ClassFunctionLp.lean. The [Finite G] shadow of the statement is that the irreducible characters of a finite group are a basis of its class functions.

• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 2.
• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC (2016), §5.2.

theorem TauCeti.ContRepresentation.inner_matrixCoeffLp_map_map {𝕜 : 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] {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ classFunctionLp 𝕜 𝕜 2 (haarProb G)) (h : G) (v w : V) : inner 𝕜 (π.matrixCoeffLp hπ ((π h) v) ((π h) w)) f = inner 𝕜 (π.matrixCoeffLp hπ v w) f

A class function does not see a simultaneous move of the two defining vectors. Moving both vectors of a matrix coefficient by π h reparametrizes it by the conjugation g ↦ h⁻¹ * g * h, which fixes a class function and preserves the inner product.

theorem TauCeti.ContRepresentation.exists_forall_inner_matrixCoeffLp_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 ⇑π) [IsAlgClosed 𝕜] (hunitary : π.IsUnitary) (hirr : (ContRepresentation.toRepresentation 𝕜 G V π).IsIrreducible) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ classFunctionLp 𝕜 𝕜 2 (haarProb G)) : ∃ (c : 𝕜), ∀ (v w : V), inner 𝕜 (π.matrixCoeffLp hπ v w) f = c * inner 𝕜 w v

Against a class function, the matrix coefficients of an irreducible collapse to one scalar. For π irreducible unitary and f a class function there is a c with ⟪(π)_{v,w}, f⟫ = c · ⟪w, v⟫ for all v, w.

The pairing is ⟪w, T v⟫ for an endomorphism T of the carrier, and TauCeti.ContRepresentation.inner_matrixCoeffLp_map_map makes T an intertwiner; Schur's lemma over an algebraically closed field turns it into a scalar.

theorem ContRepresentation.invLpₗᵢ_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] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) {ι : Type u_4} [Fintype ι] (e : OrthonormalBasis ι 𝕜 V) : (TauCeti.invLpₗᵢ 𝕜) (π.characterLp hπ) = ∑ a : ι, π.matrixCoeffLp hπ (e a) (e a)

Inverting the argument turns the character into the sum of the diagonal matrix coefficients. The character of a unitary representation satisfies χ g⁻¹ = conj (χ g), and the conjugate of a character is the sum of its diagonal matrix coefficients (ContRepresentation.star_character). This is the identity that lets a statement about the characters be read off the Peter-Weyl basis, whose blocks are spanned by the matrix coefficients themselves.

theorem TauCeti.ContRepresentation.inner_matrixCoeffLp_inv_eq_zero_of_inner_characterLp_eq_zero {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (m : IrrepModel 𝕜 G) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ classFunctionLp 𝕜 𝕜 2 (haarProb G)) (horth : inner 𝕜 (m.rep.characterLp ⋯) f = 0) (v w : EuclideanSpace 𝕜 (Fin m.dim)) : inner 𝕜 (m.rep.matrixCoeffLp ⋯ v w) ((invLpₗᵢ 𝕜) f) = 0

Vanishing against a character kills every matrix coefficient in its irreducible block. For an irreducible model, a class function pairs with all matrix coefficients of its inverse- translate through one scalar. The sum of the diagonal pairings is its pairing with the character, so that scalar vanishes when the character pairing does.

theorem TauCeti.eq_zero_of_forall_inner_characterLp_eq_zero {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} [IsAlgClosed 𝕜] (h : IsIrrepSkeleton models) {f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))} (hf : f ∈ classFunctionLp 𝕜 𝕜 2 (haarProb G)) (horth : ∀ (i : ι), inner 𝕜 ((models i).rep.characterLp ⋯) f = 0) : f = 0

Class-function completeness. A class function in L²(G) orthogonal to the character of every model in a skeleton of the unitary dual is zero.

The argument runs on the inverse-translate f(·⁻¹), which is again a class function: inversion turns the pairing against a character into the pairing against the sum of the diagonal matrix coefficients, which by TauCeti.ContRepresentation.exists_forall_inner_matrixCoeffLp_eq is dim V_i times the single scalar that the whole block contributes to. That scalar therefore vanishes, so the inverse-translate is orthogonal to the whole Peter-Weyl basis.

noncomputable def TauCeti.characterFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (i : ι) : ↥(classFunctionLp 𝕜 𝕜 2 (haarProb G))

The characters of a family of models, inside the class functions. A character is a class function (ContRepresentation.characterLp_mem_classFunctionLp), so it is an element of classFunctionLp and not merely of L²(G); the class-function completeness below is a statement about this family.

Equations

• TauCeti.characterFamily models i = ⟨(models i).rep.characterLp ⋯, ⋯⟩

@[simp]

theorem TauCeti.coe_characterFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (models : ι → IrrepModel 𝕜 G) (i : ι) : ↑(characterFamily models i) = (models i).rep.characterLp ⋯

theorem TauCeti.orthonormal_characterFamily {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (hne : Pairwise fun (i j : ι) => IsEmpty ((models i).rep.Equiv (models j).rep)) : Orthonormal 𝕜 (characterFamily models)

The characters of a pairwise inequivalent family are orthonormal in the class functions. This is the character orthogonality of ContRepresentation.orthonormal_characterLp, read inside the subspace, where the inner product is the restriction of the one on L²(G). Only inequivalence is used; exhaustivity of a skeleton is what the completeness below needs.

theorem TauCeti.orthogonal_span_characterFamily_eq_bot {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : (Submodule.span 𝕜 (Set.range (characterFamily models)))ᗮ = ⊥

The characters of a skeleton are complete in the class functions. Their span is dense: its orthogonal complement inside classFunctionLp vanishes, which is TauCeti.eq_zero_of_forall_inner_characterLp_eq_zero.

noncomputable def TauCeti.characterBasis {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : HilbertBasis ι 𝕜 ↥(classFunctionLp 𝕜 𝕜 2 (haarProb G))

The irreducible characters are a Hilbert basis of the class functions. For a skeleton of the unitary dual of a compact Hausdorff group, the characters of the models are an orthonormal basis of the closed subspace classFunctionLp of L²(G).

This is the "central" restriction of Peter-Weyl: a class function sees only the trace direction of each block of the Peter-Weyl basis, and that direction is spanned by the character. For a finite group it is the statement that the irreducible characters are a basis of the class functions.

Equations

• TauCeti.characterBasis h = HilbertBasis.mkOfOrthogonalEqBot ⋯ ⋯

@[simp]

theorem TauCeti.coe_characterBasis {𝕜 : Type u_1} {G : Type u_2} {ι : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {models : ι → IrrepModel 𝕜 G} (h : IsIrrepSkeleton models) : ⇑(characterBasis h) = characterFamily models

The class-function basis is the characters. As for TauCeti.coe_peterWeylBasis, the elements are on the nose the characters of the models, not merely some orthonormal basis whose existence is asserted.

noncomputable def TauCeti.stdCharacterBasis (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : HilbertBasis (IrrepClass 𝕜 G) 𝕜 ↥(classFunctionLp 𝕜 𝕜 2 (haarProb G))

The class-function basis, unconditionally. The characters of the models chosen in the unitary equivalence classes are a Hilbert basis of classFunctionLp; no skeleton is assumed, TauCeti.isIrrepSkeleton_model supplies one.

Equations

• TauCeti.stdCharacterBasis 𝕜 G = TauCeti.characterBasis ⋯

@[simp]

theorem TauCeti.coe_stdCharacterBasis (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : ⇑(stdCharacterBasis 𝕜 G) = characterFamily IrrepClass.model

The unconditional class-function basis is the characters of the chosen representatives.