Physicslib4.GNS.Irreducibility

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

An irreducible representation: every bounded operator commuting with all π(a) is a multiple of 1.

The operators that commute with every π(a) form the commutant π(A)'. Irreducibility asks that π(A)' consist of the scalars c·1 only. For a representation on a Hilbert space this is equivalent to the absence of a nontrivial closed subspace invariant under all π(a), because the orthogonal projection onto such a subspace lies in π(A)'; the library uses the commutant form. A state is pure exactly when its GNS representation is irreducible (isPure_iff_isIrreducible), and π is irreducible exactly when π(A)'' is all of B(H) (isIrreducible_iff_gnsVonNeumann_eq_univ).

Implementation note: on the zero Hilbert space every operator is 0 = 0·1, so every representation on it is irreducible in this sense; the usual convention excludes H = 0, and results that need a nonzero space assume it.

Blueprint: def:irreducible-representation

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 pure state: every positive functional dominated by ω is a scalar multiple of ω.

A positive functional ψ is dominated by ω when 0 ≤ ψ(a* a) ≤ ω(a* a) for every a ∈ A. If ω = t ω₁ + (1 − t) ω₂ is a mixture of states with 0 < t < 1, then t ω₁ is dominated by ω, so a pure state is not a nontrivial mixture; the converse holds too, so pure means an extreme point of the convex set of states (isPure_iff_isExtremePoint). On the algebra of bounded operators of a Hilbert space, the vector state a ↦ ⟨ψ, aψ⟩ is pure and a density matrix of rank two or more is not. A state is pure exactly when its GNS representation is irreducible (isPure_iff_isIrreducible).

Implementation note: the dominated ψ range over continuous linear functionals A →L[ℂ] ℂ, which is no restriction since positive functionals on a C*-algebra are continuous. The inequality ψ(a* a) ≤ ω(a* a) is in Mathlib's order on ℂ, so the difference is real and non-negative. This order form avoids normalising the parts of a convex combination.

Blueprint: def:pure-state

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 π(A)'' generated by a representation π, as a set of operators.

The commutant S' of a set S of bounded operators is the set of operators commuting with every element of S, and S'' = (S')' is its bicommutant. By von Neumann's density theorem every element of π(A)'' is a strong-operator limit of elements of π(A) (exists_forall_norm_sub_lt_of_mem_bicommutant), so π(A)'' adds to the represented observables their limits, such as spectral projections. π is irreducible exactly when π(A)'' is all of B(H) (isIrreducible_iff_gnsVonNeumann_eq_univ).

Implementation note: the commutant is Set.centralizer, taken in the bounded operators on H. The name refers to the GNS representation, but π is any representation. The bundled version is gnsVonNeumannAlgebra.

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 S'' of a self-adjoint set S of bounded operators, as a von Neumann algebra.

If S is closed under adjoints, then S' is a *-subalgebra of B(H) and S'' = (S')' is again one. It equals its own bicommutant, because S''' = S'. This builds the von Neumann algebra π(A)'' of a representation (gnsVonNeumannAlgebra) and the local von Neumann algebras R(B) of a net.

Implementation note: Mathlib's VonNeumannAlgebra is a *-subalgebra of the bounded operators equal to its own bicommutant. The algebra here is the commutant of the *-closed set S' (starSubalgebraCentralizer), and S'''' = S'' comes from Set.centralizer_centralizer_centralizer.

Blueprint: lmm:bicommutant-of-selfadjoint-is-von-neumann

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 π(A)'' generated by a representation π, bundled as a von Neumann algebra.

The image π(A) is closed under adjoints, since π(a)* = π(a*), so its bicommutant is a von Neumann algebra (vonNeumannOfSelfAdjoint). Its underlying set is gnsVonNeumann π (coe_gnsVonNeumannAlgebra), and its commutant is the commutant π(A)' of the representation (commutant_gnsVonNeumannAlgebra).

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.

theorem Physicslib4.GNS.isAbelian_iff_le_commutant {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : (∀ x ∈ R, ∀ y ∈ R, x * y = y * x) ↔ R ≤ R.commutant

A von Neumann algebra is abelian iff it is contained in its own commutant. R is commutative (every pair of its elements commutes) exactly when R ≤ R'. This is essentially definitional: R ≤ R' unfolds, via VonNeumannAlgebra.commutant (modelled by Set.centralizer), to the statement that every element of R commutes with every element of R.

theorem Physicslib4.GNS.bicommutant_inter_commutant_eq {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : (↑R ∩ (↑R).centralizer).centralizer.centralizer = ↑R ∩ (↑R).centralizer

The center R ∩ R' is bicommutant-closed. For a von Neumann algebra R, the intersection R ∩ R' equals its own bicommutant, so it is again a von Neumann algebra. The proof mirrors the relative-commutant construction: R = R'', so R ∩ R' = (R')' ∩ R', a centralizer of a union, hence closed under the triple centralizer law.

theorem Physicslib4.GNS.bicommutant_inter_eq {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M N : VonNeumannAlgebra H) : (↑M ∩ ↑N).centralizer.centralizer = ↑M ∩ ↑N

The intersection of two von Neumann algebras is bicommutant-closed. For von Neumann algebras M and N on H, the set M ∩ N equals its own bicommutant, so it is again a von Neumann algebra.

Unlike bicommutant_inter_commutant_eq, here M and N are arbitrary and need not form a commutant pair: since M = M'' and N = N'', the intersection is (M' ∪ N')', a centralizer, and centralizers are closed under the triple centralizer law.

noncomputable def Physicslib4.GNS.vonNeumannCenter {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : VonNeumannAlgebra H

The center Z(R) = R ∩ R' of a von Neumann algebra R.

The center consists of the elements of R that commute with all of R. It is again a von Neumann algebra, and it is abelian (vonNeumannCenter_isAbelian). R is a factor when its center is the scalars (isFactor_iff_center_eq_scalars). In quantum field theory, nontrivial central elements are observables that commute with every observable, such as the superselection charges.

Implementation note: Mathlib's VonNeumannAlgebra has no meet, so the center is built as the meet of the *-subalgebras of R and of its commutant; its underlying set is R ∩ R' (coe_vonNeumannCenter).

Blueprint: def:von-neumann-center

Equations

• Physicslib4.GNS.vonNeumannCenter R = { toStarSubalgebra := R.toStarSubalgebra ⊓ R.commutant.toStarSubalgebra, centralizer_centralizer' := ⋯ }

@[simp]

theorem Physicslib4.GNS.coe_vonNeumannCenter {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : ↑(vonNeumannCenter R) = ↑R ∩ (↑R).centralizer

The underlying set of the center is R ∩ R'.

theorem Physicslib4.GNS.vonNeumannCenter_isAbelian {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) (x : H →L[ℂ] H) : x ∈ vonNeumannCenter R → ∀ y ∈ vonNeumannCenter R, x * y = y * x

The center of a von Neumann algebra is abelian. Any two elements of Z(R) = R ∩ R' commute: each lies in R', so commutes with everything in R, in particular with the other (which lies in R).

theorem Physicslib4.GNS.vonNeumannCenter_eq_self_iff_isAbelian {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : vonNeumannCenter R = R ↔ ∀ x ∈ R, ∀ y ∈ R, x * y = y * x

R is abelian iff it equals its own center. Z(R) = R exactly when R ⊆ R', i.e. when R is abelian.

theorem Physicslib4.GNS.isAbelian_iff_eq_scalars_of_isFactor {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) (hfac : IsFactor ↑R) : (∀ x ∈ R, ∀ y ∈ R, x * y = y * x) ↔ ↑R = scalarOperators H

A factor is abelian iff it is the scalars. If a factor R (with trivial center R ∩ R' = ℂ·1) is abelian then its center is all of R, forcing R = ℂ·1; conversely the scalars are abelian.

theorem Physicslib4.GNS.vonNeumannCenter_eq_commutant {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : vonNeumannCenter R = vonNeumannCenter R.commutant

A von Neumann algebra and its commutant share the same center. Z(R) = Z(R'): R ∩ R' = R' ∩ R''= R' ∩ R, using commutativity of intersection and R'' = R.

theorem Physicslib4.GNS.isFactor_iff_center_eq_scalars {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H) : IsFactor ↑R ↔ ↑(vonNeumannCenter R) = scalarOperators H

A von Neumann algebra is a factor iff its center is the scalars. Restates the definition of a factor through the bundled center: ↑(vonNeumannCenter R) = R ∩ R'.