A bit on von Neumann algebras

This file contains two simple results about von Neumann algebras.

theorem VonNeumannAlgebra.star_commutant_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {e : H →L[ℂ] H} : star e ∈ M.commutant ↔ e ∈ M.commutant

theorem VonNeumannAlgebra.elem_idempotent_iff_ker_and_range_invariantUnder_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (e : H →L[ℂ] H) (h : IsIdempotentElem e) : e ∈ M ↔ ∀ y ∈ M.commutant, (↑e).ker.InvariantUnder ↑y ∧ (↑e).range.InvariantUnder ↑y

a continuous linear map e is in the von Neumann algebra M if and only if e.ker and e.range are M' (i.e., the commutant of M or M.centralizer) invariant subspaces

def VonNeumannAlgebra.ofHilbertSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : VonNeumannAlgebra H

The algebra of all bounded linear operators on a Hilbert space as a von Neumann algebra.

Equations

• VonNeumannAlgebra.ofHilbertSpace = { carrier := Set.univ, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯, centralizer_centralizer' := ⋯ }