Theorems · Theorem · functional analysis

VonNeumannAlgebra.IsIdempotentElem.mem_iff

∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {e : H →L[ℂ] H},
  IsIdempotentElem e →
    ∀ (S : VonNeumannAlgebra H),
      e ∈ S ↔ ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y ∧ (↑e).ker ∈ Module.End.invtSubmodule ↑y

An idempotent is an element in a von Neumann algebra if and only if its range and kernel are invariant under the commutant.

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

1 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace