The tensor product of continuous representations

The tensor product of two continuous representations of the same monoid acts by g ↦ (π g) ⊗ (ρ g), that is, by Mathlib's TensorProduct.mapL. This file builds it and proves the three facts its use requires: the operator-valued action stays continuous, unitarity is preserved, and the matrix coefficients multiply, (π ⊗ ρ)_{v ⊗ v', w ⊗ w'} = π_{v,w} · ρ_{v',w'}.

The last identity is the reason the construction is here: it is what makes the span of the matrix coefficients of all finite-dimensional representations of G closed under multiplication, hence a subalgebra of C(G, 𝕜) rather than only a subspace.

Mathlib's inner product on V ⊗[𝕜] W (TensorProduct.instInnerProductSpace) is the one for which ⟪v ⊗ₜ v', w ⊗ₜ w'⟫ = ⟪v, w⟫ * ⟪v', w'⟫, so no choice is being made here; the same file supplies TensorProduct.mapL with its multiplicativity TensorProduct.mapL_mul and its norm bound.

Main definitions

• ContRepresentation.tprod: the tensor product π ⊗ ρ of two continuous representations.

Main statements

• ContRepresentation.continuous_tprod and ContRepresentation.IsUnitary.tprod: the tensor product of continuous representations is continuous, and of unitary ones is unitary.
• ContRepresentation.matrixCoeff_tprod: matrix coefficients of a tensor product at pure tensors are products of matrix coefficients.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

noncomputable def ContRepresentation.tprod {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) : ContRepresentation 𝕜 G (TensorProduct 𝕜 V W)

The tensor product of two continuous representations, acting by g ↦ (π g) ⊗ (ρ g).

Equations

• π.tprod ρ = { toMonoidHom := { toFun := fun (g : G) => TensorProduct.mapL (π g) (ρ g), map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem ContRepresentation.tprod_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (g : G) : (π.tprod ρ) g = TensorProduct.mapL (π g) (ρ g)

The action operators of a tensor product of representations.

theorem ContRepresentation.continuous_tprod {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hπ : Continuous ⇑π) (hρ : Continuous ⇑ρ) : Continuous ⇑(π.tprod ρ)

The tensor product of two continuous representations has a continuous operator-valued action: mapL is the composition of two contractions of the separate actions.

theorem ContRepresentation.IsUnitary.tprod {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] {π : ContRepresentation 𝕜 G V} {ρ : ContRepresentation 𝕜 G W} (hπ : π.IsUnitary) (hρ : ρ.IsUnitary) : (π.tprod ρ).IsUnitary

The tensor product of two unitary representations is unitary: the tensor product of two linear isometries is a linear isometry.

@[simp]

theorem ContRepresentation.matrixCoeff_tprod {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Monoid G] [TopologicalSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hπ : Continuous ⇑π) (hρ : Continuous ⇑ρ) (v w : V) (v' w' : W) : (π.tprod ρ).matrixCoeff ⋯ (v ⊗ₜ[𝕜] v') (w ⊗ₜ[𝕜] w') = π.matrixCoeff hπ v w * ρ.matrixCoeff hρ v' w'

Matrix coefficients multiply under tensor product. The matrix coefficient of π ⊗ ρ at a pair of pure tensors is the product of the matrix coefficients of π and of ρ.