Theorems · Inductive type · functional analysis

VonNeumannAlgebra

(H : Type u) → [inst : NormedAddCommGroup H] → [InnerProductSpace ℂ H] → [CompleteSpace H] → Type u

The double commutant definition of a von Neumann algebra, as a \*-closed subalgebra of bounded operators on a Hilbert space, which is equal to its double commutant. Note that this definition is parameterised by the Hilbert space on which the algebra faithfully acts, as is standard in the literature. See WStarAlgebra for the abstract notion (a C⋆-algebra with Banach space predual). Note this is a bundled structure, parameterised by the Hilbert space H, rather than a typeclass on the type of elements. Thus we can't say that the bounded operators H →L[ℂ] H form a VonNeumannAlgebra (although we will later construct the instance WStarAlgebra (H →L[ℂ] H)), and instead will use ⊤ : VonNeumannAlgebra H.

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

16 results in Mathlib

Foundations

Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace