The representative ring is dense in C(G): the analytic core of Peter-Weyl

The representative ring 𝓡(G) of TauCeti/RepresentationTheory/Continuous/Representative.lean is the span, inside C(G, 𝕜), of the matrix coefficients of the finite-dimensional continuous representations of G. This file proves that on a compact group it is uniformly dense in C(G, 𝕜); no separation axiom is needed for density, only for the point-separation corollaries below, which read closedness of points off isClosed_singleton and so ask for [T1Space G]. That density is the analytic core of the Peter-Weyl theorem: it is what makes the matrix coefficients span a dense subspace of L²(G), and hence what a Hilbert basis of L²(G) can be assembled from.

Two halves already available meet here, and neither of them presupposes any separation property of 𝓡(G).

• Every convolution k * f by a symmetric kernel lies in the uniform closure of 𝓡(G) (TauCeti.convolutionCLM_mem_closure_representativeSubmodule). This is the spectral half: the eigenspaces of the compact self-adjoint operator convolutionOperator k span a dense subspace of L²(G), each of them is finite-dimensional and translation invariant, hence carries a finite-dimensional continuous representation, and the continuous representative of an eigenvector is one of its matrix coefficients.
• Convolution against a mollifying kernel supported near the identity moves a continuous function by an arbitrarily small amount in the uniform norm (TauCeti.exists_isMollifier_norm_convolutionCLM_toLp_sub_le), and a mollifying kernel is symmetric (TauCeti.IsMollifier.inv_apply_eq_conj). This is the approximate-identity half.

Putting them together, a continuous function is a uniform limit of functions in the closure of 𝓡(G), so it lies in that closure: TauCeti.dense_representativeSubmodule.

Point separation is a corollary, never an input. Once density is known, and provided the points of G are closed, 𝓡(G) separates the points of G because C(G, 𝕜) does: the values 0 and 1 of a Urysohn function at two distinct points cannot both be approximated to within 1/2 by a function taking equal values there. Closed points are exactly what this last step needs, and nothing before it, which is why only the results below carry [T1Space G]. Since a span separates two points only if one of its generators does, this upgrades to the statement that the finite-dimensional continuous representations themselves separate the points of a compact Hausdorff group (TauCeti.exists_contRepresentation_apply_ne): distinct group elements act differently in some finite-dimensional continuous representation.

Finally the density is transported to L²(G). The continuous functions are dense in L² of a finite measure on a compact space (ContinuousMap.toLp_denseRange) and 𝓡(G) is uniformly dense in them, so the images of the matrix coefficients span a dense subspace of L²(G), whose orthogonal complement is therefore trivial. That vanishing complement is the hypothesis of HilbertBasis.mkOfOrthogonalEqBot, so it is the form used to construct the Peter-Weyl Hilbert basis.

Implementation notes

The uniform density and the point separation drawn from it are purely topological statements, so they take no measurable structure on G: the Haar measure their proofs run through is built on the Borel σ-algebra installed inside those proofs. Only the L² statements name a measure, and they alone carry [MeasurableSpace G] [BorelSpace G].

The separation hypothesis on the point-separation results is spelled [T1Space G], the closedness of points that the Urysohn step consumes, rather than [T2Space G]. On a topological group the two are the same condition: such a group is regular (IsTopologicalGroup.regularSpace), so T1Space G already delivers T3Space G. These are therefore the usual compact Hausdorff statements, with the separation axiom stated at the strength the proof actually uses.

Main statements

• TauCeti.dense_representativeSubmodule: the Peter-Weyl density theorem. The representative ring is uniformly dense in C(G, 𝕜).
• TauCeti.representativeStarSubalgebra_dense: the same, read on the representative *-subalgebra: its topological closure is everything.
• TauCeti.representativeStarSubalgebra_separatesPoints: point separation, as a corollary.
• TauCeti.exists_contRepresentation_apply_ne: a compact Hausdorff group has enough finite-dimensional representations. Two distinct elements act differently in some finite-dimensional continuous representation.
• TauCeti.dense_image_toLp_representativeSubmodule and TauCeti.orthogonal_map_toLp_representativeSubmodule_eq_bot: the representative ring is dense in L²(G), equivalently its orthogonal complement there vanishes.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC (2016), §5.2.
• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 2.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter III.

Uniform density

theorem TauCeti.dense_representativeSubmodule (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : Dense ↑(representativeSubmodule 𝕜 G)

The Peter-Weyl density theorem. The representative ring 𝓡(G) of a compact group is uniformly dense in C(G, 𝕜). Hausdorffness is not needed: the mollifiers the proof runs on are built without it.

theorem TauCeti.representativeSubmodule_topologicalClosure_eq_top (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : (representativeSubmodule 𝕜 G).topologicalClosure = ⊤

The representative ring is dense, read as an equality of submodules: its topological closure is the whole of C(G, 𝕜).

theorem TauCeti.representativeStarSubalgebra_dense (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : (representativeStarSubalgebra 𝕜 G).topologicalClosure = ⊤

The representative *-subalgebra is dense in C(G, 𝕜). The span carrying the algebra structure is the same set as TauCeti.representativeSubmodule, so this is TauCeti.dense_representativeSubmodule again; stating it on the *-subalgebra is what makes it available to the Stone-Weierstrass vocabulary.

Point separation

theorem TauCeti.exists_mem_representativeSubmodule_apply_ne {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T1Space G] (x y : G) (hxy : x ≠ y) : ∃ f ∈ representativeSubmodule 𝕜 G, f x ≠ f y

The representative ring separates the points of a compact Hausdorff group.

Point separation is a corollary of TauCeti.dense_representativeSubmodule, and the non-circular route to Peter-Weyl depends on its never being assumed beforehand.

theorem TauCeti.representativeStarSubalgebra_separatesPoints {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T1Space G] (x y : G) (hxy : x ≠ y) : ∃ f ∈ representativeStarSubalgebra 𝕜 G, f x ≠ f y

The representative *-subalgebra separates points.

theorem TauCeti.exists_isRepresentative_apply_ne {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T1Space G] (x y : G) (hxy : x ≠ y) : ∃ (f : C(G, 𝕜)), IsRepresentative f ∧ f x ≠ f y

A single representative function already separates two distinct points, and not merely a linear combination of representative functions.

theorem TauCeti.exists_contRepresentation_apply_ne {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T1Space G] (x y : G) (hxy : x ≠ y) : ∃ (n : ℕ) (π : ContRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin n))), Continuous ⇑π ∧ π x ≠ π y

A compact Hausdorff group has enough finite-dimensional representations. Two distinct elements of G act differently in some finite-dimensional continuous representation.

This is the group-theoretic content of Peter-Weyl density: the finite-dimensional continuous representations of a compact Hausdorff group are jointly faithful.

Density in L²(G)

theorem TauCeti.dense_image_toLp_representativeSubmodule (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : Dense (⇑(ContinuousMap.toLp 2 (haarProb G) 𝕜) '' ↑(representativeSubmodule 𝕜 G))

The representative ring is dense in L²(G).

theorem TauCeti.map_toLp_representativeSubmodule_topologicalClosure_eq_top (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : (Submodule.map (↑(ContinuousMap.toLp 2 (haarProb G) 𝕜)) (representativeSubmodule 𝕜 G)).topologicalClosure = ⊤

The image of the representative ring in L²(G) has topological closure everything.

theorem TauCeti.orthogonal_map_toLp_representativeSubmodule_eq_bot (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : (Submodule.map (↑(ContinuousMap.toLp 2 (haarProb G) 𝕜)) (representativeSubmodule 𝕜 G))ᗮ = ⊥

The matrix coefficients have trivial orthogonal complement in L²(G). This is the form in which the density is consumed by HilbertBasis.mkOfOrthogonalEqBot, which turns an orthonormal system with vanishing orthogonal complement into a Hilbert basis; Schur orthogonality supplies the orthonormality, and this supplies the completeness.