Von Neumann bicommutant theorem

TheoremFinite-dimensional bicommutant theorem#✓fully proved

Let \(n\) be a natural number and let \(S\) be a unital \(*\)-subalgebra of the algebra \(M_n(\mathbb{C})\) of complex \(n \times n\) matrices. Then the commutant of the commutant of \(S\) equals \(S\): a matrix commutes with every matrix that commutes with all elements of \(S\) if and only if it lies in \(S\).

theorem bicommutant_finiteDimensional_matrix (n : ℕ)
    (S : StarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ)) :
    StarSubalgebra.centralizer ℂ
        ((StarSubalgebra.centralizer ℂ (S : Set (Matrix (Fin n) (Fin n) ℂ)) :
          Set (Matrix (Fin n) (Fin n) ℂ))) = S

Sources

• John von Neumann, "Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren", Mathematische Annalen 102 (1930), 370--427, DOI 10.1007/BF01782352. This is the finite-dimensional specialization: in finite dimension every subspace is closed, so the strong-operator closure condition of the general theorem is vacuous.

TheoremVon Neumann's double commutant theorem#●ready to prove

Let \(H\) be a complex Hilbert space and let \(S\) be a unital \(*\)-subalgebra of the algebra of bounded linear operators on \(H\). Write \(S'\) for the commutant of \(S\), the set of bounded operators on \(H\) that commute with every element of \(S\). The following are equivalent: \(S\) equals its double commutant \(S''\); \(S\) is closed in the weak operator topology; \(S\) is closed in the strong operator topology, the topology of pointwise convergence on \(H\).

public theorem_wanted vonNeumann_doubleCommutant_tfae
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    List.TFAE
      [ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))) = S
      , IsClosed
          (ContinuousLinearMapWOT.ofCLM '' (S : Set (H →L[ℂ] H)))
      , IsClosed
          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
            (S : Set (H →L[ℂ] H))) ]

Sources

• J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Math. Ann. 102 (1929) (double commutant theorem). Problem vonneumann_double_commutant of the lean-eval benchmark.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.