The von Neumann algebra generated by a set of operators

For a set s of bounded operators on a complex Hilbert space, VonNeumannAlgebra.adjoin s is the double commutant of s ∪ star s. A triple commutant equals the single commutant, so this star subalgebra is equal to its own double commutant, and it is the smallest von Neumann algebra containing s (VonNeumannAlgebra.adjoin_le_iff). Its commutant is the commutant of s ∪ star s. The set s and the star algebra it generates generate the same von Neumann algebra (VonNeumannAlgebra.adjoin_starAlgebraAdjoin).

When s is the range of a representation of a C⋆-algebra, adjoin s is the von Neumann algebra π(A)'' of the representation. Conjugation by a unitary that normalizes s preserves adjoin s (VonNeumannAlgebra.conj_mem_adjoin); this is how a unitarily implemented automorphism of π(A) extends to π(A)''.

Mathlib's VonNeumannAlgebra is the concrete double-commutant notion, so no von Neumann density theorem is used here.

noncomputable def VonNeumannAlgebra.adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : VonNeumannAlgebra H

The von Neumann algebra generated by a set s of bounded operators: the double commutant of s ∪ star s.

@[simp]

theorem VonNeumannAlgebra.coe_adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : ↑(adjoin s) = (s ∪ star s).centralizer.centralizer

The generated von Neumann algebra is the double commutant of s ∪ star s.

theorem VonNeumannAlgebra.coe_commutant_adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : ↑(adjoin s).commutant = (s ∪ star s).centralizer

The commutant of the generated von Neumann algebra is the commutant of s ∪ star s.

theorem VonNeumannAlgebra.subset_adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : s ⊆ ↑(adjoin s)

A set is contained in the von Neumann algebra it generates.

@[simp]

theorem VonNeumannAlgebra.adjoin_le_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} {M : VonNeumannAlgebra H} : adjoin s ≤ M ↔ s ⊆ ↑M

The generated von Neumann algebra is the smallest von Neumann algebra containing s.

theorem VonNeumannAlgebra.adjoin_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s t : Set (H →L[ℂ] H)} (h : s ⊆ t) : adjoin s ≤ adjoin t

Generating von Neumann algebras is monotone.

theorem VonNeumannAlgebra.coe_adjoin_of_star_subset {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} (hs : star s ⊆ s) : ↑(adjoin s) = s.centralizer.centralizer

The von Neumann algebra generated by a set closed under adjoints is its double commutant.

@[simp]

theorem VonNeumannAlgebra.adjoin_starAlgebraAdjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : adjoin ↑(StarAlgebra.adjoin ℂ s) = adjoin s

A set and the star algebra it generates generate the same von Neumann algebra.

theorem VonNeumannAlgebra.conj_mem_adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} {u : H →L[ℂ] H} (hu : u ∈ unitary (H →L[ℂ] H)) (hs : ∀ x ∈ s, u * x * star u ∈ s) {x : H →L[ℂ] H} (hx : x ∈ adjoin s) : u * x * star u ∈ adjoin s

Conjugation by a unitary u preserves the von Neumann algebra generated by s when it maps s into itself.