Guidance on GNS Construction/Gelfand-Naimark Theorem

Stream: general

[Gregory Wickham]

I have been working on formalizing the GNS construction and Gelfand-Naimark theorem. You can see my work at gw90/ThesisProjectRepo on GitHub.

I believe I have finished formalizing the GNS construction, so the natural next step would be to use it to formalize the Gelfand-Naimark theorem, but it seems that a good portion of the underlying theory I would need to do that is not yet formalized.

Specifically, I need the definition of states on a C*-algebra, and a proof that a linear functional f is a state iff it's op norm = 1 = f (1_A). (Alternatively this could suffice as a definition). But, more importantly, I need the existence of a state f_a such that

$$|f_a(a)|=\|a\|_A$$

for all self adjoint a in A (the C*-algebra). The proof of this might not be too bad when all is said and done, but I would like to try to avoid using the continuous functional calculus in Lean just because the api looks intimidating, but if someone who is more familiar with it advises me that it may be easier to use than I expect, I will reconsider.

I would also need to be able to construct a Hilbert space as a direct sum of Hilbert spaces, which I believe is also not particularly easily accomplished in Lean. (If I am incorrect about this, I would be very happy to be corrected.)

Alternatively, it might be possible to side-step some work if I can assume A is separable so that I can show it is *-isomorphic to a subalgebra of the bounded operators on l^2 for which I think there is already some theory in mathlib, but I haven't really looked into what that proof would entail, and I'm reluctant to sacrifice any more of the already fairly limited generality of my proof.

I only have about one semester (150 hours total) to complete this project, or more accurately, half a semester, because at least half will be spent on writing, so it may be a better use of my time to try to get my code mathlib-ready and just aim to merge the GNS construction alone into mathlib.

So, can anybody with more knowledge of C*-algebras and Lean advise me as to what path may be most fruitful for me to pursue, or most useful to others, in the limited time I have?

[Yaël Dillies]

cc @Jireh Loreaux

[Alex Meiburg]

Just chiming in to say I would love, love to see this. :) Great project!

[Jireh Loreaux]

Gregory Wickham said:

The proof of this might not be too bad when all is said and done, but I would like to try to avoid using the continuous functional calculus in Lean just because the api looks intimidating, but if someone who is more familiar with it advises me that it may be easier to use than I expect, I will reconsider.

I think it's much less intimidating than you might expect. Writing new API may be slightly more intimidating, but even that is not so bad once you learn the format. In any case, I'm happy to help here.

I think showing that every positive element in a C⋆-algebra has a positive linear functional which attains its norm at that element would be an excellent little project.

I've looked at your Construction.lean file. There's a number of issues with it, but probably the best way for me to address them is if you open a PR about it.

[Gregory Wickham]

Jireh Loreaux said:

I've looked at your Construction.lean file. There's a number of issues with it, but probably the best way for me to address them is if you open a PR about it.

Are you saying that I should make a PR into Mathlib? If so, should it just be essentially all of what I have so far (i.e. the content of HelperTheorems.lean, Construction.lean, and Morphisms.lean) organized into the appropriate locations? This would be my first contribution, but I'll work through the Contributing to Mathlib guide and start fixing the style, so I should be able make the PR within the next few days.

[Jireh Loreaux]

You can just leave the PR as a draft. I can then find time to review it, and with a PR it's easy to leave comments at specific places of your code.

[Gregory Wickham]

Sounds good! It was quicker to make the PR than I expected, so here is the link, https://github.com/leanprover-community/mathlib4/pull/33116, and I believe I mentioned you in a comment on it, so you may have been notified on GitHub too.