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, (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] : VonNeumannAlgebra 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' := ⋯ }