AbelianCyclicCommutant.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A cyclic commutative von Neumann algebra is maximal abelian

The proof uses only the cyclic vector. On the commutant, the norms of an operator and its adjoint at this vector agree. This controls right multiplication while approximating by the original commutative algebra.

theorem OAI.KadisonKastler.abelian_operator_norm_star line 26
theorem OAI.KadisonKastler.commutant_adjoint_vector_le line 33
theorem OAI.KadisonKastler.commutant_vector_norm_star line 57
theorem OAI.KadisonKastler.commutant_mul_comm_of_cyclic_commutative line 63
theorem OAI.KadisonKastler.mem_of_mem_commutant_of_cyclic_commutative line 107
Source documentation
In a cyclic representation, a commutative algebra equals its commutant.
```
theorem mem_of_mem_commutant_of_cyclic_commutative (S : H →L[ℂ] H)
    (hS : S ∈ M.commutant) : S ∈ M := by
…
```