Matrix coefficients of continuous representations

This file defines the matrix coefficient g ↦ ⟪π g v, w⟫ of a representation whose operator-valued action is continuous, and develops its algebra: sesquilinearity in the defining vectors, the matrix-multiplication identity at a product of group elements, the behaviour under left and right translation of the group argument, the involution coming from inversion, and the uniform bound for unitary representations.

Mathlib's ContRepresentation bundles continuous linear action operators but does not require continuity of the map from the acting topological monoid to those operators. The continuity hypothesis is therefore explicit in matrixCoeff and its API; since it is a Prop argument, two matrix coefficients built from different continuity proofs are equal by proof irrelevance.

Main definitions

• ContRepresentation.matrixCoeff: the matrix coefficient g ↦ ⟪π g v, w⟫ as an element of C(G, 𝕜).
• ContRepresentation.matrixCoeffₛₗ: the matrix coefficients of a fixed representation bundled as a sesquilinear map V →ₗ⋆[𝕜] V →ₗ[𝕜] C(G, 𝕜), in Mathlib's innerₛₗ convention.

Main statements

• ContRepresentation.matrixCoeff_apply_mul_eq_sum: in an orthonormal basis, matrix coefficients multiply like matrices, π_{ik}(g * h) = ∑ j, π_{ij}(g) · π_{jk}(h).
• ContRepresentation.matrixCoeff_comp_mulRight and ContRepresentation.matrixCoeff_comp_mulLeft: right and left translates of a matrix coefficient of π are again matrix coefficients of π. This is the G × G-action that structures the span of the matrix coefficients.
• ContRepresentation.star_matrixCoeff: the conjugate of a matrix coefficient of a unitary representation is a matrix coefficient composed with inversion.
• ContRepresentation.matrixCoeff_trivial: the matrix coefficients of the trivial representation are constant.
• ContRepresentation.norm_matrixCoeff_le: the uniform bound ‖v‖ * ‖w‖ for a unitary representation.

This algebra makes the span of the matrix coefficients of a fixed representation a translation-stable subspace of C(G), stable under conjugation followed by inversion of the argument, and it feeds the Schur orthogonality relations. Conjugation alone leaves that span in general: it produces a matrix coefficient of the contragredient representation. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapters 2–4.

noncomputable def ContRepresentation.matrixCoeff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : C(G, 𝕜)

The matrix coefficient g ↦ ⟪π g v, w⟫ of a representation with continuous operator-valued action.

Equations

• π.matrixCoeff hπ v w = { toFun := fun (g : G) => inner 𝕜 ((π g) v) w, continuous_toFun := ⋯ }

@[simp]

theorem ContRepresentation.matrixCoeff_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) (g : G) : (π.matrixCoeff hπ v w) g = inner 𝕜 ((π g) v) w

Evaluation of a matrix coefficient.

theorem ContRepresentation.matrixCoeff_apply_one {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : (π.matrixCoeff hπ v w) 1 = inner 𝕜 v w

A matrix coefficient at the identity is the inner product of its defining vectors.

Sesquilinearity in the defining vectors

Following Mathlib's inner-product convention, a matrix coefficient is conjugate-linear in its first vector and linear in its second.

@[simp]

theorem ContRepresentation.matrixCoeff_zero_left {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (w : V) : π.matrixCoeff hπ 0 w = 0

@[simp]

theorem ContRepresentation.matrixCoeff_zero_right {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) : π.matrixCoeff hπ v 0 = 0

@[simp]

theorem ContRepresentation.matrixCoeff_add_left {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v₁ v₂ w : V) : π.matrixCoeff hπ (v₁ + v₂) w = π.matrixCoeff hπ v₁ w + π.matrixCoeff hπ v₂ w

@[simp]

theorem ContRepresentation.matrixCoeff_add_right {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w₁ w₂ : V) : π.matrixCoeff hπ v (w₁ + w₂) = π.matrixCoeff hπ v w₁ + π.matrixCoeff hπ v w₂

@[simp]

theorem ContRepresentation.matrixCoeff_smul_left {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (c : 𝕜) (v w : V) : π.matrixCoeff hπ (c • v) w = (starRingEnd 𝕜) c • π.matrixCoeff hπ v w

@[simp]

theorem ContRepresentation.matrixCoeff_smul_right {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) (c : 𝕜) (w : V) : π.matrixCoeff hπ v (c • w) = c • π.matrixCoeff hπ v w

noncomputable def ContRepresentation.matrixCoeffₛₗ {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : V →ₗ⋆[𝕜] V →ₗ[𝕜] C(G, 𝕜)

The matrix coefficients of a fixed representation, bundled as a sesquilinear map: conjugate linear in the first vector, linear in the second, exactly as Mathlib's innerₛₗ.

Bundling records the sesquilinearity in the form the span of the matrix coefficients is built from, and supplies the remaining additive identities (map_neg, map_sub, map_sum) through the LinearMap API.

Equations

• π.matrixCoeffₛₗ hπ = { toFun := fun (v : V) => { toFun := π.matrixCoeff hπ v, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContRepresentation.matrixCoeffₛₗ_apply_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : ((π.matrixCoeffₛₗ hπ) v) w = π.matrixCoeff hπ v w

Translating the group argument

theorem ContRepresentation.matrixCoeff_apply_mul_right {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) (g g₀ : G) : (π.matrixCoeff hπ v w) (g * g₀) = (π.matrixCoeff hπ ((π g₀) v) w) g

Translating the argument of a matrix coefficient on the right moves the action onto the first vector. The pointwise statement needs no continuity of the multiplication of G.

theorem ContRepresentation.matrixCoeff_apply_mul_eq_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {ι : Type u_4} [Fintype ι] (e : OrthonormalBasis ι 𝕜 V) (v w : V) (g h : G) : (π.matrixCoeff hπ v w) (g * h) = ∑ i : ι, (π.matrixCoeff hπ (e i) w) g * (π.matrixCoeff hπ v (e i)) h

Matrix coefficients multiply like matrices: expanding the intermediate vector π h v in an orthonormal basis writes the coefficient at a product as a sum of products of coefficients. In the basis notation π_{ij}(g) = ⟪π g eⱼ, eᵢ⟫ this is π_{ik}(g * h) = ∑ j, π_{ij}(g) · π_{jk}(h).

The trivial representation, and restriction along a homomorphism

@[simp]

theorem ContRepresentation.matrixCoeff_trivial {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (v w : V) : (trivial 𝕜 G V).matrixCoeff ⋯ v w = ContinuousMap.const G (inner 𝕜 v w)

A matrix coefficient of the trivial representation is the constant function at the inner product of its defining vectors; the trivial action is constant, so continuous_const is its continuity witness. Which constants arise depends on V: they are the values of the inner product, so all of 𝕜 when some ⟪v, w⟫ ≠ 0, and only 0 when V is trivial.

@[simp]

theorem ContRepresentation.matrixCoeff_subrepresentation {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {W : Submodule 𝕜 V} (hW : ∀ (g : G), ∀ v ∈ W, (π g) v ∈ W) (v w : ↥W) : (π.subrepresentation W hW).matrixCoeff ⋯ v w = π.matrixCoeff hπ ↑v ↑w

A matrix coefficient of an invariant submodule is the matrix coefficient of the ambient representation at the underlying vectors, so passing to a subrepresentation creates no new matrix coefficients; continuous_subrepresentation hπ is the continuity witness of the restricted action.

@[simp]

theorem ContRepresentation.matrixCoeff_restrict {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {H : Type u_4} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (v w : V) : (π.restrict φ).matrixCoeff ⋯ v w = (π.matrixCoeff hπ v w).comp { toFun := ⇑φ, continuous_toFun := hφ }

Restricting a representation along a continuous homomorphism precomposes its matrix coefficients; the restricted action is π ∘ φ, so hπ.comp hφ is its continuity witness.

@[simp]

theorem ContRepresentation.matrixCoeff_comp_mulRight {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [SeparatelyContinuousMul G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) (g₀ : G) : (π.matrixCoeff hπ v w).comp (ContinuousMap.mulRight g₀) = π.matrixCoeff hπ ((π g₀) v) w

The right translate of a matrix coefficient of π is again a matrix coefficient of π: the translation is absorbed into the first vector.

theorem ContRepresentation.matrixCoeff_apply_mul_left {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (v w : V) (g₀ g : G) : (π.matrixCoeff hπ v w) (g₀ * g) = (π.matrixCoeff hπ v ((π g₀⁻¹) w)) g

Translating the argument of a matrix coefficient of a unitary representation on the left moves the action of the inverse onto the second vector.

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

Evaluating a matrix coefficient of a unitary representation at an inverse conjugates it and swaps its defining vectors. This is the involution that the span of the matrix coefficients carries; see star_matrixCoeff for the packaged form.

@[simp]

theorem ContRepresentation.matrixCoeff_comp_mulLeft {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} [SeparatelyContinuousMul G] (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (v w : V) (g₀ : G) : (π.matrixCoeff hπ v w).comp (ContinuousMap.mulLeft g₀) = π.matrixCoeff hπ v ((π g₀⁻¹) w)

The left translate of a matrix coefficient of a unitary representation is again a matrix coefficient: the translation is absorbed into the second vector.

@[simp]

theorem ContRepresentation.star_matrixCoeff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {π : ContRepresentation 𝕜 G V} [ContinuousInv G] (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (v w : V) : star (π.matrixCoeff hπ v w) = (π.matrixCoeff hπ w v).comp { toFun := Inv.inv, continuous_toFun := ⋯ }

The conjugate of a matrix coefficient of a unitary representation is the matrix coefficient with its vectors swapped, precomposed with inversion. So the span of the matrix coefficients of a unitary representation is stable under the star operation of C(G, 𝕜) followed by inversion of the argument.

theorem ContRepresentation.norm_matrixCoeff_le {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [CompactSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) (v w : V) : ‖π.matrixCoeff hπ v w‖ ≤ ‖v‖ * ‖w‖

The uniform norm of a matrix coefficient of a unitary representation is at most the product of the norms of its defining vectors.