Double commutant theorem

Stream: mathlib4

[Boris Bilich]

I have recently formalized the double commutant theorem: #35538 . However, in the current form, it is not yet stated as a theorem about VonNeumannAlgebra. I don't understand bundled structures well. How to correctly formalize the statement "StarSubalgebra which is WOT-closed is a von Neumann algebra."?

[Jireh Loreaux]

I've assigned this to myself, but I won't be able to review it until next week. The way to formalize that statement would be to have a def which produces vonNeumannAlgebra and takes as input a StarSubalgebra and proof that it is WOT closed. But please refrain from doing this for now. The PR is already very long as is, and it's going to need lots of cleaning up before its ready for primetime, so adding new material will only slow down the review process.

[Jireh Loreaux]

One thing that could help speed review is to add comments to the code outlining the steps of the proofs. The proofs you have written are quite long, and probably that means things should be factored out into lemmas, but I won't know until I have time to look thoroughly next week.

[Boris Bilich]

@Jireh Loreaux thanks! I will try to improve readability until the next week.