A bit on von Neumann algebras #

This file contains two simple results about von Neumann algebras.

theorem von_neumann_algebra.has_idempotent_iff_ker_and_range_are_invariant_under_commutant {H : Type u_1} [normed_add_comm_group H] [inner_product_space ℂ H] [complete_space H] (M : von_neumann_algebra H) (e : H →L[ℂ ] H) (h : is_idempotent_elem e) :

e ∈ M ↔ ∀ (y : H →L[ℂ ] H), y ∈ M.commutant → (linear_map.ker e.to_linear_map).invariant_under ↑y ∧ (linear_map.range e.to_linear_map).invariant_under ↑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

source

def von_neumann_algebra.of_Hilbert_space {H : Type u_1} [normed_add_comm_group H] [inner_product_space ℂ H] [complete_space H] :

von_neumann_algebra 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

von_neumann_algebra.of_Hilbert_space = {carrier := set.univ (H →L[ℂ ] H), mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _, star_mem' := _, centralizer_centralizer' := _}