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}
:
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, (LinearMap.ker ↑e).InvariantUnder ↑y ∧ (LinearMap.range ↑e).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]
:
By definition, the bounded linear operators on a Hilbert space H form a von Neumann algebra.
!!(But the note on the definition says that we can't do this because it's a bundled structure?)!! idk?
Equations
- VonNeumannAlgebra.ofHilbertSpace = { carrier := Set.univ, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯, centralizer_centralizer' := ⋯ }