K theory

Stream: new members

[Omar Mohsen]

Kevin Buzzard said:

Usually people say "what are you interested in contributing?" before giving access, but clearly Omar has friends in the right places :-)

I plan to write about C* algebras and Banach algebras in general, mostly in the spectrum and star file.
Mostly a proof of Gelfand's isomorphism for commutative C* algebras (I can't seem to find it in mathlib).
If I don't find the experience too miserable I might do Bott periodicity in K theory for C* algebras (certainly not in mathlib)

[Anatole Dedecker]

Gelfand's isomorphism is docs#gelfandStarTransform right? Or do you mean something else?

[Anatole Dedecker]

Ah, maybe you want the nonunital version. I'm not sure wether we have it.

[Jireh Loreaux]

Hey @Omar Mohsen, I noticed when I gave you access that we had similar interests. We have the (unbundled, i.e., not in terms of docs#CategoryTheory.category) Gelfand duality, including the natural isomorphisms, for unital C star algebras, as Anatole mentioned. We don't yet have the non-unital version, which is a bit more subtle than most people make it out to be (because it's really just the unital version with specified points). But ultimately I think we have most of the ingredients.

Let's coordinate. I can tell you what exists, and what doesn't, and we'll find something you're interested in to do.

[Omar Mohsen]

@Jireh Loreaux Hey, sure we should coordinate. My ultimate interest is Bott periodicity for K theory of C* algebras. For this one needs some functional calculus, hence my interest in Gelfand's isomorphism.

For the moment, I am looking at the Todo list from docs#gelfandStarTransform, as well as the ToDo list from the matrices file on infinite products. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html#Matrix

If you already have a branch you are working on then I would be glad to work with you.

[Jireh Loreaux]

Yes, Bott periodicity is a long-term target for me as well. I'll have an update tomorrow on the continuous functional calculus, and I'll ping you when I send it.

[Jireh Loreaux]

The other thing we need is two-sided ideals. There's a thread about this, and a GitHub project for it. I don't have time today to describe what needs to be done, but maybe I'll have some time tomorrow for that.

[Jireh Loreaux]

Note, we already have the isomorphism docs#continuousFunctionalCalculus, but it's not quite ready to be used. We also have spectral permanence. The docs#Unitization has the C star norm, but I recently ran into some type class issues with it. Hopefully that will be sorted soon.

[Anatole Dedecker]

To expand on why "it's not quite ready to be used": we have all the required mathematics to do functional calculus (except maybe uniqueness, but it's not hard to prove), the point is that we want to make it as easy to use as possible. Jireh spent a large amount of time thinking about it and trying various approaches, and I think the final iteration should land in Mathlib rather soon.

[Anatole Dedecker]

I would love to see K-theory in mathlib! Obviously I have much less experience with the mathematics than both of you, but I did follow the course of Georges Skandalis on the subject so I'd love to help setting up the theory!

[Notification Bot]

Ruben Van de Velde has marked this topic as unresolved.

[Notification Bot]

10 messages were moved here from #new members > ✔ Write access non-master branches by Ruben Van de Velde.