Von Neumann algebras

We give the "abstract" and "concrete" definitions of a von Neumann algebra. We still have a major project ahead of us to show the equivalence between these definitions!

An abstract von Neumann algebra WStarAlgebra M is a C^* algebra with a Banach space predual, per Sakai (1971).

A concrete von Neumann algebra VonNeumannAlgebra H (where H is a Hilbert space) is a *-closed subalgebra of bounded operators on H which is equal to its double commutant.

We'll also need to prove the von Neumann double commutant theorem, that the concrete definition is equivalent to a *-closed subalgebra which is weakly closed.

class WStarAlgebra (M : Type u) [NormedRing M] [StarRing M] [CstarRing M] [Module ℂ M] [NormedAlgebra ℂ M] [StarModule ℂ M] : Prop

Sakai's definition of a von Neumann algebra as a C^* algebra with a Banach space predual.

So that we can unambiguously talk about these "abstract" von Neumann algebras in parallel with the "concrete" ones (weakly closed *-subalgebras of B(H)), we name this definition WStarAlgebra.

Note that for now we only assert the mere existence of predual, rather than picking one. This may later prove problematic, and need to be revisited. Picking one may cause problems with definitional unification of different instances. One the other hand, not picking one means that the weak-* topology (which depends on a choice of predual) must be defined using the choice, and we may be unhappy with the resulting opaqueness of the definition.

• exists_predual : ∃ (X : Type u) (x : NormedAddCommGroup X) (x_1 : NormedSpace ℂ X) (_ : CompleteSpace X), Nonempty (NormedSpace.Dual ℂ X ≃ₗᵢ⋆[ℂ] M)

  There is a Banach space X whose dual is isometrically (conjugate-linearly) isomorphic to the WStarAlgebra.

theorem WStarAlgebra.exists_predual {M : Type u} [NormedRing M] [StarRing M] [CstarRing M] [Module ℂ M] [NormedAlgebra ℂ M] [StarModule ℂ M] [self : WStarAlgebra M] : ∃ (X : Type u) (x : NormedAddCommGroup X) (x_1 : NormedSpace ℂ X) (_ : CompleteSpace X), Nonempty (NormedSpace.Dual ℂ X ≃ₗᵢ⋆[ℂ] M)

There is a Banach space X whose dual is isometrically (conjugate-linearly) isomorphic to the WStarAlgebra.

structure VonNeumannAlgebra (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] extends StarSubalgebra : 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.

• carrier : Set (H →L[ℂ] H)
• mul_mem' : ∀ {a b : H →L[ℂ] H}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' : ∀ {a b : H →L[ℂ] H}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' : ∀ (r : ℂ), (algebraMap ℂ (H →L[ℂ] H)) r ∈ self.carrier
• star_mem' : ∀ {a : H →L[ℂ] H}, a ∈ self.carrier → star a ∈ self.carrier
• centralizer_centralizer' : self.carrier.centralizer.centralizer = self.carrier

  The double commutant (a.k.a. centralizer) of a VonNeumannAlgebra is itself.

theorem VonNeumannAlgebra.centralizer_centralizer' {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (self : VonNeumannAlgebra H) : self.carrier.centralizer.centralizer = self.carrier

The double commutant (a.k.a. centralizer) of a VonNeumannAlgebra is itself.

instance VonNeumannAlgebra.instSetLike {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : SetLike (VonNeumannAlgebra H) (H →L[ℂ] H)

Equations

• VonNeumannAlgebra.instSetLike = { coe := fun (S : VonNeumannAlgebra H) => S.carrier, coe_injective' := ⋯ }

noncomputable instance VonNeumannAlgebra.instStarMemClass {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : StarMemClass (VonNeumannAlgebra H) (H →L[ℂ] H)

Equations

• ⋯ = ⋯

instance VonNeumannAlgebra.instSubringClass {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : SubringClass (VonNeumannAlgebra H) (H →L[ℂ] H)

Equations

• ⋯ = ⋯

@[simp]

theorem VonNeumannAlgebra.mem_carrier {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : VonNeumannAlgebra H} {x : H →L[ℂ] H} : x ∈ S.toStarSubalgebra ↔ x ∈ ↑S

@[simp]

theorem VonNeumannAlgebra.coe_toStarSubalgebra {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : ↑S.toStarSubalgebra = ↑S

@[simp]

theorem VonNeumannAlgebra.coe_mk {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : StarSubalgebra ℂ (H →L[ℂ] H)) (h : S.carrier.centralizer.centralizer = S.carrier) : ↑{ toStarSubalgebra := S, centralizer_centralizer' := h } = ↑S

theorem VonNeumannAlgebra.ext {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : VonNeumannAlgebra H} {T : VonNeumannAlgebra H} (h : ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T) : S = T

@[simp]

theorem VonNeumannAlgebra.centralizer_centralizer {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : (↑S).centralizer.centralizer = ↑S

def VonNeumannAlgebra.commutant {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : VonNeumannAlgebra H

The centralizer of a VonNeumannAlgebra, as a VonNeumannAlgebra.

Equations

• S.commutant = { toStarSubalgebra := StarSubalgebra.centralizer ℂ ↑S, centralizer_centralizer' := ⋯ }

@[simp]

theorem VonNeumannAlgebra.coe_commutant {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : ↑S.commutant = (↑S).centralizer

@[simp]

theorem VonNeumannAlgebra.mem_commutant_iff {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : VonNeumannAlgebra H} {z : H →L[ℂ] H} : z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

@[simp]

theorem VonNeumannAlgebra.commutant_commutant {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : S.commutant.commutant = S