Physicslib4.GNS.DirectSum

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 ⊕ᵢ πᵢ of a family of representations, acting on the Hilbert direct sum ⊕ᵢ Hᵢ.

A vector of ⊕ᵢ Hᵢ is a family x = (xᵢ) with xᵢ ∈ Hᵢ and Σᵢ ‖xᵢ‖² < ∞, and the direct sum acts componentwise, (⊕ᵢ πᵢ)(a) x = (πᵢ(a) xᵢ)ᵢ: a block-diagonal operator with blocks πᵢ(a). It is bounded by ‖a‖, because each πᵢ(a) is (a -homomorphism of C-algebras is contractive). Each summand is a subrepresentation (intertwines_single), and the projection onto it lies in the commutant (summandProj_mem_commutant), so a direct sum of two nonzero representations is reducible (not_isIrreducible_directSum).

Implementation note: the Hilbert direct sum is Mathlib's ℓ²-space lp H 2, and the operator is the diagonal lpDiag of the family πᵢ(a). The index type ι is arbitrary.

Blueprint: def:direct-sum-representation

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 π.