Direct sums of representations

Given a family of *-representations π i : A →⋆ₐ[ℂ] (H i →L[ℂ] H i) of a C*-algebra A on Hilbert spaces H i, the direct-sum representation ⊕ᵢ πᵢ acts on the ℓ²-direct sum lp H 2 by the diagonal operator of fun i ↦ π i a (uniformly bounded by ‖a‖, since a *-homomorphism of C*-algebras is contractive).

This file builds directSum π : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) and proves the two basic structural facts:

• intertwines_single — each summand embeds as a subrepresentation: the isometric inclusion H j ↪ lp H 2 intertwines π j with directSum π;
• summandProj_mem_commutant — the orthogonal projection onto the j-th summand lies in the commutant of directSum π, so a direct sum of two or more nonzero summands is reducible.

Coordinate evaluation

noncomputable def Physicslib4.GNS.lpEvalCLM {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] (j : ι) : ↥(lp H 2) →L[ℂ] H j

Coordinate evaluation x ↦ x j as a continuous linear map lp H 2 →L H j (norm ≤ 1).

Equations

• Physicslib4.GNS.lpEvalCLM j = { toFun := fun (x : ↥(lp H 2)) => ↑x j, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem Physicslib4.GNS.lpEvalCLM_apply {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] (j : ι) (x : ↥(lp H 2)) : (lpEvalCLM j) x = ↑x j

The direct-sum representation

noncomputable def Physicslib4.GNS.directSumFun {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) (a : A) : ↥(lp H 2) →L[ℂ] ↥(lp H 2)

The value of the direct-sum representation on a: the diagonal operator of the family fun i ↦ π i a, uniformly bounded by ‖a‖.

Equations

• Physicslib4.GNS.directSumFun π a = Physicslib4.lpDiag (fun (i : ι) => (π i) a) ⋯ ⋯

@[simp]

theorem Physicslib4.GNS.directSumFun_apply_coe {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) (a : A) (x : ↥(lp H 2)) (i : ι) : ↑((directSumFun π a) x) i = ((π i) a) (↑x i)

noncomputable def Physicslib4.GNS.directSum {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) : A →⋆ₐ[ℂ] ↥(lp H 2) →L[ℂ] ↥(lp H 2)

The direct-sum representation ⊕ᵢ πᵢ on the ℓ²-direct sum lp H 2.

Equations

• Physicslib4.GNS.directSum π = { toFun := Physicslib4.GNS.directSumFun π, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem Physicslib4.GNS.directSum_apply {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) (a : A) : (directSum π) a = directSumFun π a

Subrepresentations and commutant projections

theorem Physicslib4.GNS.intertwines_single {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} [DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) (j : ι) : Intertwines (π j) (directSum π) (lp.singleContinuousLinearMap ℂ H 2 j)

Each summand is a subrepresentation: the isometric inclusion H j ↪ lp H 2 intertwines π j with the direct-sum representation.

noncomputable def Physicslib4.GNS.summandProj {ι : Type u_2} [DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] (j : ι) : ↥(lp H 2) →L[ℂ] ↥(lp H 2)

The orthogonal projection onto the j-th summand, x ↦ single j (x j).

Equations

• Physicslib4.GNS.summandProj j = lp.singleContinuousLinearMap ℂ H 2 j ∘SL Physicslib4.GNS.lpEvalCLM j

@[simp]

theorem Physicslib4.GNS.summandProj_apply {ι : Type u_2} [DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] (j : ι) (x : ↥(lp H 2)) : (summandProj j) x = lp.single 2 j (↑x j)

theorem Physicslib4.GNS.summandProj_mem_commutant {A : Type u_1} [CStarAlgebra A] {ι : Type u_2} [DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) (j : ι) : summandProj j ∈ (Set.range ⇑(directSum π)).centralizer

The projection onto the j-th summand commutes with the whole representation, hence lies in the commutant of directSum π.