Conversation
… they are WStarClosed subalgebras, but then appeals to the result that such subalgebras have preduals.
| % The space $\Omega$ is called the \textbf{spectrum space} of $\mathcal{A}$. | ||
| % \end{corollary} | ||
|
|
||
| We state the following without proof, as it is available in Mathlib. |
There was a problem hiding this comment.
Was this meant to be commented out too?
There was a problem hiding this comment.
Yes, because we (so far) haven't needed nonunital Gelfand, and Jireh advised against putting in the cfc_n because it's already in mathlib. So I think it's ok to get rid of all of this. I commented it out in case we weren't sure...
There was a problem hiding this comment.
Oh yes, and also the last theorem commented out here points at the Gelfand duality. I was leaving all this here and commented out since we seem to be able to get away with CFC arguments...and we are probably going to keep getting away with them...
There was a problem hiding this comment.
What I meant was that this line isn't commented out, was it not meant to be commented out?
But, yeah, I don't know, you can keep things commented out I guess, just in case.
There was a problem hiding this comment.
I see. Yeah, that seemed silly there. Must have missed it.
|
Can you merge master and add the label for |
2 participants
Mild blueprint cleanup. (Not strictly dependent on #74, but if we wait for that to merge, I can also include it.)