Physicslib4.GNS.Amplification

Amplification and reducibility of direct sums

Two consequences of the direct-sum construction (Physicslib4.GNS.DirectSum):

• Reducibility. The summand projections lie in the commutant, so if the direct-sum representation is irreducible they must be scalars (summandProj_isScalar_of_isIrreducible); consequently a direct sum with two summands carrying nonzero vectors is reducible (not_isIrreducible_directSum).
• Amplification. The ι-fold amplification ι · π := ⊕_{ι} π of a single representation, in which π embeds as each summand (amplification_intertwines_single).

The quasi-equivalence π ~ ι · π

The quasi-equivalence of a representation with its amplification (QuasiEquiv π (ι · π)) is not proved here. It requires a *-isomorphism of the generated von Neumann algebras π(A)'' ≃⋆ₐ (ι·π)(A)''. The natural map is T ↦ lpDiag (fun _ ↦ T) (the diagonal), which is an injective *-homomorphism carrying π a ↦ (ι·π) a; but surjectivity onto (ι·π)(A)'' is exactly the amplification commutant theorem (π ⊗ 1)' = π' ⊗ B(K) (equivalently (π ⊗ 1)'' = π'' ⊗ ℂ1), a von Neumann algebra result that Mathlib does not provide.

Reducibility

theorem Physicslib4.GNS.summandProj_isScalar_of_isIrreducible {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) (hirr : IsIrreducible (directSum π)) (j : ι) : summandProj j ∈ scalarOperators ↥(lp H 2)

If the direct-sum representation is irreducible, each summand projection is a scalar operator (irreducibility means the commutant is trivial).

theorem Physicslib4.GNS.not_isIrreducible_directSum {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 k : ι} (hjk : j ≠ k) {v : H j} (hv : v ≠ 0) {w : H k} (hw : w ≠ 0) : ¬IsIrreducible (directSum π)

A direct sum with two summands carrying nonzero vectors is reducible: the projection onto one summand is a non-scalar element of the commutant.

Amplification

noncomputable def Physicslib4.GNS.amplification {A : Type u_1} [CStarAlgebra A] {H₀ : Type u_2} [NormedAddCommGroup H₀] [InnerProductSpace ℂ H₀] [CompleteSpace H₀] {ι : Type u_3} (π : A →⋆ₐ[ℂ] H₀ →L[ℂ] H₀) : A →⋆ₐ[ℂ] ↥(lp (fun (x : ι) => H₀) 2) →L[ℂ] ↥(lp (fun (x : ι) => H₀) 2)

The amplification ι·π of a representation π: the direct sum of copies of π indexed by ι.

It acts on the Hilbert direct sum ℓ²(ι, H₀) of copies of H₀, by π(a) in every copy, that is, on H₀ ⊗ ℓ²(ι) by π(a) ⊗ 1. It is π with multiplicity |ι|: π embeds in it as each summand (amplification_intertwines_single), and with two or more copies on a nonzero space it is reducible (not_isIrreducible_directSum).

Implementation note: amplification is directSum of the constant family. That π and ι·π are quasi-equivalent is not proved; it needs the commutant of an amplification, (π ⊗ 1)' = π' ⊗ B(ℓ²(ι)), which Mathlib does not provide.

Blueprint: def:amplification

Equations

• Physicslib4.GNS.amplification π = Physicslib4.GNS.directSum fun (x : ι) => π

theorem Physicslib4.GNS.amplification_intertwines_single {A : Type u_1} [CStarAlgebra A] {H₀ : Type u_2} [NormedAddCommGroup H₀] [InnerProductSpace ℂ H₀] [CompleteSpace H₀] {ι : Type u_3} [DecidableEq ι] (π : A →⋆ₐ[ℂ] H₀ →L[ℂ] H₀) (j : ι) : Intertwines π (amplification π) (lp.singleContinuousLinearMap ℂ (fun (x : ι) => H₀) 2 j)

In the amplification, π embeds as each summand: the isometric inclusion of the j-th copy H₀ ↪ ℓ²(ι, H₀) intertwines π with ι · π.