The representative ring of a monoid with a topology

A representative function on a monoid G equipped with a topology is a matrix coefficient of a finite-dimensional continuous representation of G. Their span TauCeti.representativeSubmodule is the representative ring 𝓡(G) ⊆ C(G, 𝕜), and the point of this file is that the span is far more than a subspace: it is a *-subalgebra, TauCeti.representativeStarSubalgebra.

Three constructions supply the three closure properties, and each is a statement about representations rather than about functions:

• the trivial representation on 𝕜 gives the constants (TauCeti.isRepresentative_one);
• the tensor product of two representations multiplies their matrix coefficients (ContRepresentation.matrixCoeff_tprod), giving closure under multiplication;
• the conjugate representation conjugates them (OrthonormalBasis.star_matrixCoeff_eq_matrixCoeff_conjugate), giving closure under the involution of C(G, 𝕜).

Characters are sums of diagonal matrix coefficients, so they lie in 𝓡(G) as well (ContRepresentation.character_mem_representativeSubmodule).

Implementation notes

The carrier of a representation cannot be quantified over all types at once, so the definition of a representative function pins the standard models EuclideanSpace 𝕜 (Fin n). Nothing is lost: TauCeti.matrixCoeff_mem_representativeSubmodule says that a matrix coefficient of a continuous representation on any finite-dimensional inner product space is a representative function, by transporting the representation along the isometry supplied by stdOrthonormalBasis (ContinuousLinearEquiv.congr). That transport lemma is what makes the pinned model harmless, and it is how the closure proofs feed the tensor product V ⊗ W and the conjugate back into the definition. Requiring the carrier to be an inner product space is no restriction on the span either: over 𝕜 every finite-dimensional space admits an inner product, and every functional on it is ⟪·, w⟫ for some w, so pairing with a functional produces no function beyond these.

No unitarity is required, of 𝓡(G) or of any lemma about it: none of the three closure properties uses it, π ⊗ ρ and the conjugate of π being available for an arbitrary continuous π. The unitary case is used for Schur orthogonality and Peter-Weyl. Preservation of unitarity is recorded with each of the three constructions (ContRepresentation.IsUnitary.tprod, OrthonormalBasis.isUnitary_conjugate, ContRepresentation.IsUnitary.congr); on a compact group the distinction is empty anyway, since Haar averaging unitarizes.

Neither TauCeti.IsRepresentative nor TauCeti.representativeSubmodule exposes its implementation. What downstream arguments need of them is supplied by TauCeti.isRepresentative_iff, which produces a representation from a representative function, and TauCeti.representativeSubmodule_eq_span, which is what an induction over the span runs on.

Point separation is deliberately absent. That 𝓡(G) separates the points of a compact G is equivalent to the Peter-Weyl theorem, so it cannot be recorded at this stage without circularity; it is a corollary of the analytic density theorem, proved in TauCeti/RepresentationTheory/Compact/RepresentativeDensity.lean, not an input to it.

Main definitions

• TauCeti.IsRepresentative: being a matrix coefficient of a finite-dimensional continuous representation.
• TauCeti.representativeSubmodule: the span of the representative functions.
• TauCeti.representativeStarSubalgebra: that span, as a *-subalgebra of C(G, 𝕜).

Main statements

• TauCeti.isRepresentative_iff and TauCeti.representativeSubmodule_eq_span: the elimination principles for the two definitions.
• TauCeti.matrixCoeff_mem_representativeSubmodule: every matrix coefficient of a finite-dimensional continuous representation lies in 𝓡(G).
• TauCeti.IsRepresentative.mul, TauCeti.IsRepresentative.star, TauCeti.isRepresentative_one, TauCeti.isRepresentative_zero: the representative functions themselves are closed under multiplication and conjugation and contain the constants and 0.
• TauCeti.mul_mem_representativeSubmodule, TauCeti.star_mem_representativeSubmodule: the same closure properties for their span.
• ContRepresentation.character_mem_representativeSubmodule: characters lie in 𝓡(G).

The uniform density of this algebra in C(G) is the analytic core of Peter-Weyl. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Chapter III.

def TauCeti.IsRepresentative {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] (f : C(G, 𝕜)) : Prop

A representative function on G: a matrix coefficient of a finite-dimensional continuous representation. The carrier is pinned to a standard model EuclideanSpace 𝕜 (Fin n), which by TauCeti.isRepresentative_matrixCoeff is no restriction.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.isRepresentative_iff {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {f : C(G, 𝕜)} : IsRepresentative f ↔ ∃ (n : ℕ) (π : ContRepresentation 𝕜 G (EuclideanSpace 𝕜 (Fin n))) (hπ : Continuous ⇑π) (v : EuclideanSpace 𝕜 (Fin n)) (w : EuclideanSpace 𝕜 (Fin n)), f = π.matrixCoeff hπ v w

Being a representative function is exhibiting the function as a matrix coefficient of a continuous representation on a standard model.

def TauCeti.representativeSubmodule (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : Submodule 𝕜 C(G, 𝕜)

The representative ring 𝓡(G), as a submodule of C(G, 𝕜): the span of the matrix coefficients of the finite-dimensional continuous representations of G.

Equations

• TauCeti.representativeSubmodule 𝕜 G = Submodule.span 𝕜 {f : C(G, 𝕜) | TauCeti.IsRepresentative f}

theorem TauCeti.representativeSubmodule_eq_span (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : representativeSubmodule 𝕜 G = Submodule.span 𝕜 {f : C(G, 𝕜) | IsRepresentative f}

The representative ring is the span of the representative functions.

theorem TauCeti.mem_representativeSubmodule_of_isRepresentative {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {f : C(G, 𝕜)} (hf : IsRepresentative f) : f ∈ representativeSubmodule 𝕜 G

A representative function lies in the representative ring.

theorem TauCeti.isRepresentative_matrixCoeff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : IsRepresentative (π.matrixCoeff hπ v w)

Every matrix coefficient is representative. A matrix coefficient of a continuous representation on an arbitrary finite-dimensional inner product space is a representative function: transporting the representation along (stdOrthonormalBasis 𝕜 V).repr puts it on a standard model without changing its matrix coefficients.

theorem TauCeti.matrixCoeff_mem_representativeSubmodule {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : π.matrixCoeff hπ v w ∈ representativeSubmodule 𝕜 G

Every matrix coefficient of a finite-dimensional continuous representation lies in 𝓡(G).

theorem TauCeti.isRepresentative_one (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : IsRepresentative 1

The constants are representative. The constant function 1 is the matrix coefficient of the trivial one-dimensional representation at the unit vector 1 : 𝕜.

theorem TauCeti.isRepresentative_zero (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : IsRepresentative 0

The zero function is representative. It is the matrix coefficient of the trivial one-dimensional representation at the zero vector.

theorem TauCeti.one_mem_representativeSubmodule (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : 1 ∈ representativeSubmodule 𝕜 G

The constant function 1 lies in 𝓡(G).

theorem TauCeti.IsRepresentative.mul {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {a b : C(G, 𝕜)} (ha : IsRepresentative a) (hb : IsRepresentative b) : IsRepresentative (a * b)

A product of representative functions is representative: the product of a matrix coefficient of π and one of ρ is a matrix coefficient of π ⊗ ρ.

theorem TauCeti.IsRepresentative.star {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {a : C(G, 𝕜)} (ha : IsRepresentative a) : IsRepresentative (Star.star a)

The conjugate of a representative function is representative: the conjugate of a matrix coefficient of π is a matrix coefficient of the conjugate of π.

theorem TauCeti.mul_mem_representativeSubmodule {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {a b : C(G, 𝕜)} (ha : a ∈ representativeSubmodule 𝕜 G) (hb : b ∈ representativeSubmodule 𝕜 G) : a * b ∈ representativeSubmodule 𝕜 G

𝓡(G) is closed under multiplication.

theorem TauCeti.star_mem_representativeSubmodule {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {a : C(G, 𝕜)} (ha : a ∈ representativeSubmodule 𝕜 G) : star a ∈ representativeSubmodule 𝕜 G

𝓡(G) is closed under the involution of C(G, 𝕜).

def TauCeti.representativeStarSubalgebra (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Monoid G] [TopologicalSpace G] : StarSubalgebra 𝕜 C(G, 𝕜)

The representative ring as a *-subalgebra of C(G, 𝕜). The span of the matrix coefficients of the finite-dimensional continuous representations of G contains the constants, and is closed under multiplication and under conjugation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mem_representativeStarSubalgebra_iff {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] {f : C(G, 𝕜)} : f ∈ representativeStarSubalgebra 𝕜 G ↔ f ∈ representativeSubmodule 𝕜 G

Membership in the representative *-subalgebra is membership in its underlying span.

theorem ContRepresentation.character_mem_representativeSubmodule {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.character hπ ∈ TauCeti.representativeSubmodule 𝕜 G

The character of a finite-dimensional continuous representation lies in 𝓡(G). Its conjugate is the sum of the diagonal matrix coefficients, and 𝓡(G) is closed under conjugation.