Characters of continuous representations

The character of a finite-dimensional representation is the function g ↦ trace (π g). Mathlib builds it for a bare Representation and proves its algebraic identities; this file packages it as an element of C(G, 𝕜) for a representation with continuous operator-valued action, and links it to the matrix coefficients of TauCeti/RepresentationTheory/Continuous/MatrixCoefficient.lean.

Main definitions

• ContRepresentation.character: the character g ↦ trace (π g) as an element of C(G, 𝕜).

Main statements

• ContRepresentation.character_one: the character at the identity is the dimension.
• ContRepresentation.character_conj: the character is a class function.
• ContRepresentation.star_character: the conjugate of the character is the sum of the diagonal matrix coefficients ∑ i, ⟪π g eᵢ, eᵢ⟫ in an orthonormal basis. The conjugation is not decoration: Mathlib's inner product is conjugate linear in its first argument, so the diagonal matrix coefficient matrixCoeff π hπ eᵢ eᵢ is ⟪π g eᵢ, eᵢ⟫, whereas the diagonal entry of the matrix of π g in that basis, which the trace sums, is ⟪eᵢ, π g eᵢ⟫.
• ContRepresentation.character_apply_inv: the character of a unitary representation at an inverse is the conjugate of its value.
• ContRepresentation.norm_character_apply_le: a unitary character is bounded by the dimension.
• ContRepresentation.continuous_character_mul_self: the character read along the squaring map g ↦ g * g is continuous.

Implementation notes

The underlying function is Mathlib's Representation.character, so the identities that are purely algebraic — the value at 1, invariance under conjugation, the behaviour under a product of group elements — are restatements of Representation.char_one, Representation.char_conj and Representation.char_mul_comm rather than new proofs. What this file adds is continuity, which Representation.character cannot see, and the orthonormal-basis bridge to matrix coefficients.

Continuity of the trace is not automatic from continuity of π alone: it is continuity of the functional T ↦ trace T on V →L[𝕜] V, which holds because that space is finite-dimensional over the complete field 𝕜. That functional is TauCeti.traceCLM of TauCeti/Analysis/Normed/Module/Trace.lean, shared with TauCeti/RepresentationTheory/Compact/Intertwiner/Basic.lean, which uses it to average a trace.

Only the trace is at stake in the sections without an inner product, so they ask no more of the scalars than that functional does: 𝕜 is a complete nontrivially normed field there, and becomes RCLike only where an orthonormal basis or unitarity enters.

The L² theory and the orthogonality relations are in TauCeti/RepresentationTheory/Compact/Character/Basic.lean. Nothing here needs a group, a measure, or compactness, so it is stated over a topological monoid. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.character {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : C(G, 𝕜)

The character g ↦ trace (π g) of a finite-dimensional representation with continuous operator-valued action, as an element of C(G, 𝕜).

The underlying function is Mathlib's Representation.character; only the continuity is new, and it comes from TauCeti.traceCLM, the trace as a continuous linear functional.

Equations

• π.character hπ = { toFun := (ContRepresentation.toRepresentation 𝕜 G V π).character, continuous_toFun := ⋯ }

theorem ContRepresentation.coe_character {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ⇑(π.character hπ) = (toRepresentation 𝕜 G V π).character

The character of a continuous representation is Mathlib's character of the underlying representation; every algebraic identity about the latter therefore applies verbatim.

@[simp]

theorem ContRepresentation.character_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g : G) : (π.character hπ) g = (LinearMap.trace 𝕜 V) ↑(π g)

Evaluation of the character.

theorem ContRepresentation.character_one {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : (π.character hπ) 1 = ↑(Module.finrank 𝕜 V)

The character at the identity is the dimension of the representation.

theorem ContRepresentation.character_mul_comm {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g h : G) : (π.character hπ) (h * g) = (π.character hπ) (g * h)

The character is unchanged by transposing a product of group elements.

@[simp]

theorem ContRepresentation.character_trivial {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : (trivial 𝕜 G V).character ⋯ = ContinuousMap.const G ↑(Module.finrank 𝕜 V)

The character of the trivial representation is the constant function at the dimension: every action operator is the identity, whose trace is the dimension. The trivial action is constant, so continuous_const is its continuity witness.

@[simp]

theorem ContRepresentation.character_restrict {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {H : Type u_4} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) : (π.restrict φ).character ⋯ = (π.character hπ).comp { toFun := ⇑φ, continuous_toFun := hφ }

Restricting a representation along a continuous homomorphism precomposes its character.

theorem ContRepresentation.character_apply_eq_sum_inner {𝕜 : 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 ⇑π) {ι : Type u_4} [Fintype ι] (e : OrthonormalBasis ι 𝕜 V) (g : G) : (π.character hπ) g = ∑ i : ι, inner 𝕜 (e i) ((π g) (e i))

The character read off an orthonormal basis: it is the sum of the diagonal entries ⟪eᵢ, π g eᵢ⟫ of the matrix of π g.

theorem ContRepresentation.star_character {𝕜 : 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 ⇑π) {ι : Type u_4} [Fintype ι] (e : OrthonormalBasis ι 𝕜 V) : star (π.character hπ) = ∑ i : ι, π.matrixCoeff hπ (e i) (e i)

The conjugate of the character is the sum of the diagonal matrix coefficients. With matrixCoeff π hπ v w g = ⟪π g v, w⟫, conjugate linear in v, the diagonal matrix coefficient πᵢᵢ(g) = ⟪π g eᵢ, eᵢ⟫ is the conjugate of the diagonal entry ⟪eᵢ, π g eᵢ⟫ summed by the trace; the conjugation on the left is what records that. This is the identity through which the Schur orthogonality relations compute inner products of characters.

theorem ContRepresentation.norm_character_apply_le {𝕜 : 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 ⇑π) (hunitary : π.IsUnitary) (g : G) : ‖(π.character hπ) g‖ ≤ ↑(Module.finrank 𝕜 V)

The character of a unitary representation is bounded by the dimension: each of the dim V diagonal entries ⟪eᵢ, π g eᵢ⟫ has modulus at most ‖eᵢ‖ * ‖π g eᵢ‖ = 1.

theorem ContRepresentation.character_conj {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Group G] [TopologicalSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g h : G) : (π.character hπ) (h * g * h⁻¹) = (π.character hπ) g

The character is a class function. This is Representation.char_conj transported to the continuous packaging.

theorem ContRepresentation.character_apply_inv {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (g : G) : (π.character hπ) g⁻¹ = (starRingEnd 𝕜) ((π.character hπ) g)

The character of a unitary representation at an inverse is the conjugate of its value: the action of g⁻¹ is the adjoint of the action of g, and taking adjoints conjugates the diagonal entries in an orthonormal basis.

The character along the squaring map

theorem ContRepresentation.continuous_character_mul_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Monoid G] [TopologicalSpace G] [ContinuousMul G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : Continuous fun (g : G) => (π.character hπ) (g * g)

The character read along the squaring map g ↦ g * g is continuous.