Matrix coefficients of a representation

The matrix coefficients of a representation ρ against a basis b of its carrier are the functions g ↦ LinearMap.toMatrix b b (ρ g) i j on the group. A property of a representation is often expressed by asking that all of them lie in some fixed algebra A of functions on the group: that they are polynomial in the entries of g, say, or bounded, or continuous.

This file collects the closure properties of such a condition that hold for every subalgebra A, so that a proof of the condition never has to be repeated for each choice:

• a surjective intertwining map carries the condition from source to target, because a basis vector of the target lifts to a vector of the source, and the entries against the target basis are then fixed linear combinations of the entries against the source basis, with coefficients read off the lift and independent of g;
• changing the basis of a single representation is the special case of the identity map, so the condition is basis independent;
• against the basis of pure tensors of basis vectors, the matrix coefficients of a tensor power of a representation are the products of matrix coefficients of the representation;
• against a tensor product of bases, the matrix coefficients of a tensor product of representations are the products of matrix coefficients of the two factors.

All but the last need only a commutative semiring of scalars; the tensor-product entries are read off TensorProduct.toMatrix_map, which Mathlib states over a commutative ring.

Main results

• Representation.toMatrix_mem_of_toMatrix_mem_of_surjective: the matrix coefficients of a quotient representation stay inside any subalgebra containing those of the source.
• Representation.toMatrix_mem_of_toMatrix_mem: changing basis keeps the matrix coefficients inside any subalgebra.
• Representation.toMatrix_tensorPower and Representation.toMatrix_tensorPower_mem: the matrix coefficients of a tensor power are products of matrix coefficients, hence stay inside any subalgebra containing those of the representation.
• Representation.toMatrix_tprod and Representation.toMatrix_tprod_mem: the matrix coefficients of a tensor product are products of matrix coefficients, hence stay inside any subalgebra containing those of the two factors.

theorem Representation.toMatrix_mem_of_toMatrix_mem_of_surjective {k : Type u} [CommSemiring k] {G : Type z} [Monoid G] {W : Type v} [AddCommMonoid W] [Module k W] {V : Type y} [AddCommMonoid V] [Module k V] (A : Subalgebra k (G → k)) {ι : Type w} [Fintype ι] [DecidableEq ι] {κ : Type x} [Fintype κ] [DecidableEq κ] (b : Module.Basis ι k W) (c : Module.Basis κ k V) {ρ : Representation k G W} {σ : Representation k G V} (f : ρ.IntertwiningMap σ) (hf : Function.Surjective ⇑f) (h : ∀ (p l : ι), (fun (g : G) => (LinearMap.toMatrix b b) (ρ g) p l) ∈ A) (i j : κ) : (fun (g : G) => (LinearMap.toMatrix c c) (σ g) i j) ∈ A

The matrix coefficients of a quotient representation stay inside any subalgebra of functions. If σ is the image of ρ under a surjective intertwining map, and every matrix coefficient of ρ against a basis of the source lies in a subalgebra A of the functions on the group, then so does every matrix coefficient of σ against a basis of the target.

theorem Representation.toMatrix_mem_of_toMatrix_mem {k : Type u} [CommSemiring k] {G : Type z} [Monoid G] {W : Type v} [AddCommMonoid W] [Module k W] (A : Subalgebra k (G → k)) {ι : Type w} [Fintype ι] [DecidableEq ι] {κ : Type x} [Fintype κ] [DecidableEq κ] (b : Module.Basis ι k W) (c : Module.Basis κ k W) (ρ : Representation k G W) (h : ∀ (p l : ι), (fun (g : G) => (LinearMap.toMatrix b b) (ρ g) p l) ∈ A) (i j : κ) : (fun (g : G) => (LinearMap.toMatrix c c) (ρ g) i j) ∈ A

Changing basis keeps the matrix coefficients inside any subalgebra of functions: if every matrix coefficient of ρ against one basis lies in a subalgebra A of the functions on the group, so does every matrix coefficient against any other basis.

theorem Representation.toMatrix_tensorPower {k : Type u} [CommSemiring k] {G : Type z} [Monoid G] {W : Type v} [AddCommMonoid W] [Module k W] {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι k W) (ρ : Representation k G W) (d : ℕ) (g : G) (i j : Fin d → ι) : (LinearMap.toMatrix (Basis.piTensorProduct fun (x : Fin d) => b) (Basis.piTensorProduct fun (x : Fin d) => b)) ((ρ.tensorPower d) g) i j = ∏ l : Fin d, (LinearMap.toMatrix b b) (ρ g) (i l) (j l)

Against the basis of pure tensors of basis vectors, a matrix coefficient of the d-fold tensor power of ρ is the product of the d matrix coefficients of ρ listed by the two indices.

theorem Representation.toMatrix_tensorPower_mem {k : Type u} [CommSemiring k] {G : Type z} [Monoid G] {W : Type v} [AddCommMonoid W] [Module k W] (A : Subalgebra k (G → k)) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι k W) {ρ : Representation k G W} {d : ℕ} (h : ∀ (p l : ι), (fun (g : G) => (LinearMap.toMatrix b b) (ρ g) p l) ∈ A) (i j : Fin d → ι) : (fun (g : G) => (LinearMap.toMatrix (Basis.piTensorProduct fun (x : Fin d) => b) (Basis.piTensorProduct fun (x : Fin d) => b)) ((ρ.tensorPower d) g) i j) ∈ A

The matrix coefficients of a tensor power stay inside any subalgebra of functions containing those of the representation.

theorem Representation.toMatrix_tprod {k : Type u} [CommRing k] {G : Type z} [Monoid G] {W : Type v} [AddCommGroup W] [Module k W] {V : Type y} [AddCommGroup V] [Module k V] {ι : Type w} [Fintype ι] [DecidableEq ι] {κ : Type x} [Fintype κ] [DecidableEq κ] (b : Module.Basis ι k W) (c : Module.Basis κ k V) {ρ : Representation k G W} {σ : Representation k G V} (g : G) (i j : ι × κ) : (LinearMap.toMatrix (b.tensorProduct c) (b.tensorProduct c)) ((ρ.tprod σ) g) i j = (LinearMap.toMatrix b b) (ρ g) i.1 j.1 * (LinearMap.toMatrix c c) (σ g) i.2 j.2

Against a tensor product of bases, the matrix coefficients of a tensor product of representations are the products of the matrix coefficients of the two factors: the Kronecker product, read entrywise.

theorem Representation.toMatrix_tprod_mem {k : Type u} [CommRing k] {G : Type z} [Monoid G] {W : Type v} [AddCommGroup W] [Module k W] {V : Type y} [AddCommGroup V] [Module k V] (A : Subalgebra k (G → k)) {ι : Type w} [Fintype ι] [DecidableEq ι] {κ : Type x} [Fintype κ] [DecidableEq κ] (b : Module.Basis ι k W) (c : Module.Basis κ k V) {ρ : Representation k G W} {σ : Representation k G V} (hb : ∀ (p l : ι), (fun (g : G) => (LinearMap.toMatrix b b) (ρ g) p l) ∈ A) (hc : ∀ (p l : κ), (fun (g : G) => (LinearMap.toMatrix c c) (σ g) p l) ∈ A) (i j : ι × κ) : (fun (g : G) => (LinearMap.toMatrix (b.tensorProduct c) (b.tensorProduct c)) ((ρ.tprod σ) g) i j) ∈ A

The matrix coefficients of a tensor product stay inside any subalgebra of functions containing those of the two factors.