Gelfand-Naimark Theorem/GNS Construction

Stream: new members

[Gregory Wickham]

Is the Gelfand-Naimark Theorem (and necessarily the GNS Construction) anywhere in mathlib or are there plans to add it?

If not, I am considering trying to formalize it myself. I'm an undergraduate student and I'm planning to do my senior thesis on formalizing something in lean, and since I've taken a course on $C^*$-algebras, when I saw that the continuous functional calculus was already in mathlib, I naturally looked for the Gelfand-Naimark theorem next, but it's not obvious to me whether it's there. Does anyone have thoughts on how feasible formalizing it would be? My current lean experience is mainly just working through the first 3-ish chapters of Mathematics in Lean (though I hope to get through a couple more chapters in the next month or so) and familiarizing myself with the $C^*$-algebra content already in mathlib.

I've also noticed that lean generally prefers proving things in as much generality as possible and possibly stating the more familiar theorems as corollaries, so does anybody know if the Stinespring dilation theorem is in mathlib or if that would be the preferred way to produce the GNS construction? Because it seems the GNS construction is one of the consequences of that theorem.

Also, does anybody know what textbook mathlib's $C^*$-algebra content is following? I haven't seen any references in the relevant documentation yet.

[Jireh Loreaux]

1. We don't have GNS yet.
2. I'm pretty sure @Anatole Dedecker has considered it though, and I think @Frédéric Dupuis is probably thinking about / working toward Stinespring.
3. regarding which textbook: it's a bit of a hodgepodge because there is no text with which I've been completely enamored. Certainly Takesaki and Bourbaki have been texts I've examined (along with Lin, Pedersen, and Davidson). But, as I plan on outlining soon, I think I'd like to follow Sakai's text for the development of W⋆-algebras (a.k.a. von Neumann algebras, but technically they are different, see docs#WStarAlgebra and docs#VonNeumannAlgebra).

See also #mathlib4 > L^infty as C*-algebra where we have had a brief discussion about the spectral theorem, among other things.