Irreducibility of representations and Schur's lemma

A *-representation π : A →⋆ₐ[ℂ] (H →L[ℂ] H) is irreducible when its commutant is trivial: the only bounded operators commuting with every π a are the scalar multiples of the identity. This is the von Neumann (commutant) form of irreducibility, the operator-algebra counterpart of "no nontrivial closed invariant subspace".

The central analytic fact is the topological Schur lemma for a cyclic representation: if T commutes with all π a and its diagonal GNS coefficient a ↦ ⟪Ω, T (π a Ω)⟫ is proportional to a ↦ ⟪Ω, π a Ω⟫, then T is the corresponding scalar. The proof is pure Hilbert-space analysis: the off-diagonal coefficients ⟪π b Ω, (T - c) (π a Ω)⟫ all vanish (using the *-representation property and the commutation relation), so (T - c) annihilates the dense cyclic orbit and is therefore zero.

This is the bridge between the commutant and the GNS state: a commutant operator is a scalar exactly when its GNS coefficient is proportional to the state.

def Physicslib4.GNS.IsIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) : Prop

A *-representation π of A on H is irreducible when its commutant is trivial: every bounded operator T commuting with all π a is a scalar multiple of the identity.

Equations

• Physicslib4.GNS.IsIrreducible π = ∀ (T : H →L[ℂ] H), (∀ (a : A), π a * T = T * π a) → ∃ (c : ℂ), T = c • 1

theorem Physicslib4.GNS.eq_smul_one_of_commute_of_cyclic {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) {T : H →L[ℂ] H} (hT : ∀ (a : A), π a * T = T * π a) {c : ℂ} (hprop : ∀ (a : A), inner ℂ Ω (T ((π a) Ω)) = c * inner ℂ Ω ((π a) Ω)) : T = c • 1

Topological Schur lemma (proportional coefficient ⟹ scalar). Let Ω be a cyclic vector for π. If T commutes with every π a and the diagonal GNS coefficient a ↦ ⟪Ω, T (π a Ω)⟫ equals c times a ↦ ⟪Ω, π a Ω⟫, then T = c • 1. The key step is that all off-diagonal coefficients ⟪π b Ω, (T - c) (π a Ω)⟫ vanish, so (T - c) kills the dense cyclic orbit.

theorem Physicslib4.GNS.isScalar_iff_coeff_proportional {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) {ω : State A} (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {T : H →L[ℂ] H} (hT : ∀ (a : A), π a * T = T * π a) : (∃ (c : ℂ), T = c • 1) ↔ ∃ (t : ℂ), ∀ (a : A), inner ℂ Ω (T ((π a) Ω)) = t * ω a

A commutant operator is a scalar iff its GNS coefficient is proportional to the state. In a cyclic representation reproducing ω, an operator T commuting with all π a is a scalar multiple of the identity exactly when its diagonal coefficient a ↦ ⟪Ω, T (π a Ω)⟫ is a scalar multiple of ω. This is the precise operator-theoretic bridge between irreducibility and purity: it is the forward (easy) direction together with the topological Schur lemma.

def Physicslib4.GNS.IsPure {A : Type u_1} [CStarAlgebra A] (ω : State A) : Prop

A state ω is pure if every positive linear functional ψ dominated by ω (i.e. 0 ≤ ψ(a* a) ≤ ω(a* a)) is a scalar multiple of ω. This is the order-theoretic characterization of purity (extreme point of the state space), phrased so that no convex-combination/normalization bookkeeping is needed.

Equations

• Physicslib4.GNS.IsPure ω = ∀ (ψ : A →L[ℂ] ℂ), (∀ (a : A), 0 ≤ ψ (star a * a)) → (∀ (a : A), ψ (star a * a) ≤ ω (star a * a)) → ∃ (t : ℂ), ∀ (a : A), ψ a = t * ω a

noncomputable def Physicslib4.GNS.coeffFunctional {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (T : H →L[ℂ] H) : A →L[ℂ] ℂ

The GNS coefficient functional a ↦ ⟪Ω, T (π a Ω)⟫ of an operator T, bundled as a continuous linear functional.

Equations

• Physicslib4.GNS.coeffFunctional π Ω T = { toFun := fun (a : A) => inner ℂ Ω (T ((π a) Ω)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖Ω‖ * ‖T‖ * ‖Ω‖) ⋯

@[simp]

theorem Physicslib4.GNS.coeffFunctional_apply {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (T : H →L[ℂ] H) (a : A) : (coeffFunctional π Ω T) a = inner ℂ Ω (T ((π a) Ω))

theorem Physicslib4.GNS.coeffFunctional_star_mul {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} {T : H →L[ℂ] H} (hT : ∀ (a : A), π a * T = T * π a) (a : A) : (coeffFunctional π Ω T) (star a * a) = inner ℂ ((π a) Ω) (T ((π a) Ω))

On an element star a * a, the coefficient functional of a commutant operator T evaluates to ⟪π a Ω, T (π a Ω)⟫.

theorem Physicslib4.GNS.isPositive_inner_nonneg {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {S : H →L[ℂ] H} (hS : S.IsPositive) (v : H) : 0 ≤ inner ℂ v (S v)

For a positive operator S, the diagonal inner product ⟪v, S v⟫ is a non-negative complex number (its real part is ≥ 0 and its imaginary part vanishes by self-adjointness).

theorem Physicslib4.GNS.scalar_of_isSelfAdjoint_of_isPure {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) (hpure : IsPure ω) {S : H →L[ℂ] H} (hSsa : IsSelfAdjoint S) (hScomm : ∀ (a : A), π a * S = S * π a) : ∃ (c : ℂ), S = c • 1

Pure ⟹ irreducible, self-adjoint case. If ω is pure (in its cyclic GNS representation reproducing ω) and S is a self-adjoint operator commuting with all π a, then S is a scalar multiple of the identity. The proof scales S into a positive operator T = r·S + ½·1 with 0 ≤ T ≤ 1, whose coefficient functional is positive and dominated by ω; purity forces it proportional to ω, so Schur's lemma makes T (hence S) a scalar.

theorem Physicslib4.GNS.isIrreducible_of_isPure {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) (hpure : IsPure ω) : IsIrreducible π

Pure ⟹ irreducible. If a state ω is pure, then any cyclic representation reproducing ω (in particular its GNS representation) is irreducible: the only operators commuting with all π a are scalars. The proof decomposes a commuting operator into its self-adjoint real and imaginary parts (the commutant is *-closed), each of which is a scalar by scalar_of_isSelfAdjoint_of_isPure.

def Physicslib4.GNS.gnsVonNeumann {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) : Set (H →L[ℂ] H)

The von Neumann algebra generated by a representation π: the bicommutant (double Set.centralizer) of the image π(A), i.e. π(A)''.

Equations

• Physicslib4.GNS.gnsVonNeumann π = (Set.range ⇑π).centralizer.centralizer

theorem Physicslib4.GNS.star_mem_setCentralizer {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} (hS : ∀ x ∈ S, star x ∈ S) {a : H →L[ℂ] H} (ha : a ∈ S.centralizer) : star a ∈ S.centralizer

The commutant (Set.centralizer) of a self-adjoint set of operators is itself self-adjoint.

theorem Physicslib4.GNS.star_mem_subalgebraCentralizer {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Set (H →L[ℂ] H)} (hT : ∀ x ∈ T, star x ∈ T) {a : H →L[ℂ] H} (ha : a ∈ Subalgebra.centralizer ℂ T) : star a ∈ Subalgebra.centralizer ℂ T

The commutant of a self-adjoint set of operators is *-closed (subalgebra form, used to build the StarSubalgebra).

noncomputable def Physicslib4.GNS.starSubalgebraCentralizer {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Set (H →L[ℂ] H)) (hT : ∀ x ∈ T, star x ∈ T) : StarSubalgebra ℂ (H →L[ℂ] H)

The commutant of a self-adjoint set of operators, packaged as a StarSubalgebra (it is a subalgebra, and *-closed by the previous lemma).

Equations

• Physicslib4.GNS.starSubalgebraCentralizer T hT = { toSubalgebra := Subalgebra.centralizer ℂ T, star_mem' := ⋯ }

@[simp]

theorem Physicslib4.GNS.coe_starSubalgebraCentralizer {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Set (H →L[ℂ] H)) (hT : ∀ x ∈ T, star x ∈ T) : ↑(starSubalgebraCentralizer T hT) = T.centralizer

theorem Physicslib4.GNS.carrier_starSubalgebraCentralizer {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Set (H →L[ℂ] H)) (hT : ∀ x ∈ T, star x ∈ T) : (starSubalgebraCentralizer T hT).carrier = T.centralizer

noncomputable def Physicslib4.GNS.vonNeumannOfSelfAdjoint {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) (hS : ∀ x ∈ S, star x ∈ S) : VonNeumannAlgebra H

The bicommutant of a self-adjoint set is a von Neumann algebra. For a self-adjoint set S of bounded operators, the double commutant S'' is a von Neumann algebra (it equals its own bicommutant, since S'''' = S'').

Equations

• Physicslib4.GNS.vonNeumannOfSelfAdjoint S hS = { toStarSubalgebra := Physicslib4.GNS.starSubalgebraCentralizer S.centralizer ⋯, centralizer_centralizer' := ⋯ }

@[simp]

theorem Physicslib4.GNS.coe_vonNeumannOfSelfAdjoint {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) (hS : ∀ x ∈ S, star x ∈ S) : ↑(vonNeumannOfSelfAdjoint S hS) = S.centralizer.centralizer

theorem Physicslib4.GNS.center_gnsVonNeumann_eq_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} (hirr : IsIrreducible π) : gnsVonNeumann π ∩ (gnsVonNeumann π).centralizer = {T : H →L[ℂ] H | ∃ (c : ℂ), T = c • 1}

An irreducible representation generates a factor. The von Neumann algebra π(A)'' of an irreducible representation has trivial center: an operator lies in the center π(A)'' ∩ (π(A)'')' if and only if it is a scalar multiple of the identity. The center is contained in (π(A)'')' = π(A)' (the triple commutant collapses to the single one), which irreducibility makes the scalars; conversely scalars are central.

theorem Physicslib4.GNS.gnsVonNeumann_eq_univ_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} (hirr : IsIrreducible π) : gnsVonNeumann π = Set.univ

An irreducible representation generates all of B(H). The von Neumann algebra π(A)'' of an irreducible representation is the whole algebra of bounded operators: gnsVonNeumann π = ⊤. By irreducibility the commutant π(A)' is the scalars, and the centralizer of the scalars is everything (every operator commutes with c • 1), so the bicommutant π(A)'' = (scalars)' = B(H). This is the density (bicommutant-theorem) form of irreducibility.

theorem Physicslib4.GNS.isIrreducible_iff_gnsVonNeumann_eq_univ {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} : IsIrreducible π ↔ gnsVonNeumann π = Set.univ

Irreducibility is equivalent to generating \mathcal B(H). A representation is irreducible iff its generated von Neumann algebra is the whole of \mathcal B(H). The forward direction is gnsVonNeumann_eq_univ_of_isIrreducible; the converse uses that \mathcal B(H) is a central ℂ-algebra (its center is the scalars): if the bicommutant is everything then every operator commutes with the commutant, so any operator commuting with π(A) is central, hence scalar.

theorem Physicslib4.GNS.range_selfAdjoint {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (x : H →L[ℂ] H) : x ∈ Set.range ⇑π → star x ∈ Set.range ⇑π

The image π(A) of a representation is self-adjoint: π is a *-homomorphism, so star (π a) = π (star a).

noncomputable def Physicslib4.GNS.gnsVonNeumannAlgebra {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) : VonNeumannAlgebra H

The von Neumann algebra generated by a representation, bundled. The bicommutant π(A)'' as a genuine VonNeumannAlgebra (the image π(A) is self-adjoint, so its bicommutant is a von Neumann algebra). Its underlying set is gnsVonNeumann π.

Equations

• Physicslib4.GNS.gnsVonNeumannAlgebra π = Physicslib4.GNS.vonNeumannOfSelfAdjoint (Set.range ⇑π) ⋯

@[simp]

theorem Physicslib4.GNS.coe_gnsVonNeumannAlgebra {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) : ↑(gnsVonNeumannAlgebra π) = gnsVonNeumann π

theorem Physicslib4.GNS.coe_gnsVonNeumannAlgebra_eq_univ_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} (hirr : IsIrreducible π) : ↑(gnsVonNeumannAlgebra π) = Set.univ

Bundled density form of irreducibility. For an irreducible representation, the bundled von Neumann algebra π(A)'' is all of 𝓑(H): its underlying set is Set.univ. Mathlib's VonNeumannAlgebra carries no lattice ⊤, so this is the faithful "= ⊤" statement at the level of the underlying set; the order-theoretic content — that it is the greatest von Neumann algebra — is gnsVonNeumannAlgebra_isGreatest_of_isIrreducible.

theorem Physicslib4.GNS.gnsVonNeumannAlgebra_isGreatest_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} (hirr : IsIrreducible π) (S : VonNeumannAlgebra H) : S ≤ gnsVonNeumannAlgebra π

The GNS von Neumann algebra of an irreducible representation is the greatest one. Its underlying set being all of 𝓑(H), every von Neumann algebra on H is contained in it. This is the order-theoretic "= ⊤" statement, available even though Mathlib does not equip VonNeumannAlgebra H with a ⊤ element.