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

• TauCeti.ContRepresentation.matrixCoeff: the matrix coefficient g ↦ ⟪π g v, w⟫ as an element of C(G, 𝕜).
• TauCeti.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

• TauCeti.ContRepresentation.matrixCoeff_apply_mul_eq_sum: in an orthonormal basis, matrix coefficients multiply like matrices, π_{ik}(g * h) = ∑ j, π_{ij}(g) · π_{jk}(h).
• TauCeti.ContRepresentation.matrixCoeff_comp_mulRight and TauCeti.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.
• TauCeti.ContRepresentation.star_matrixCoeff: the conjugate of a matrix coefficient of a unitary representation is a matrix coefficient composed with inversion.
• TauCeti.ContRepresentation.matrixCoeff_trivial: the matrix coefficients of the trivial representation are constant.
• TauCeti.ContRepresentation.norm_matrixCoeff_le: the uniform bound ‖v‖ * ‖w‖ for a unitary representation.

The algebra of matrix coefficients is the Layer 3 milestone of the compact-groups roadmap; it is what 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 of Layer 4. Conjugation alone leaves that span in general: it produces a matrix coefficient of the contragredient representation, which is not built here. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapters 2–4.

noncomputable def TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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) : matrixCoeff (ContRepresentation.trivial 𝕜 G V) ⋯ 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 TauCeti.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) : matrixCoeff (subrepresentation π W hW) ⋯ 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 TauCeti.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) : matrixCoeff (π.restrict φ) ⋯ 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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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.