K-theory

Stream: new members

[Justus Springer]

Hello!
I am an MSc student in mathematics and this is my first post here. I have a BSc degree in computer science as well as in pure mathematics. I have some experience in functional programming and the Coq proof assistant and I'm currently very excited about learning lean! I would love to contribute to mathlib at some point, when I have acquired more lean experience. Does anyone know if K-theory has been formalized yet? I have not seen anything on it in mathlib. I wonder if the definition of the K-groups of a ring or a topological space would be a feasible project as of now.

[Johan Commelin]

Nope, I don't think any K-theory has been done yet. It sounds like a nice ambitious project!

[Adam Topaz]

+1 for trying to formalize K theory. I think it would be a very challenging project.

How would you want to define it?

[Johan Commelin]

@Justus Springer Welcome btw :hello: . Which university are you at?

[Kevin Buzzard]

Another +1 for K theory. But this means several different things, right? I would imagine defining things like K1 of a ring and K2 of a field and proving basic properties about them would be easy, and doing K_n would be more challenging but not impossible. I'm talking about algebraic K theory, I don't know anything about topological K theory. I will remark that I had two students who formalised group cohomology with me in the past, first I had a BSc student who did H^0 and H^1 and proved the beginning of the long exact sequence, and then an MSc student who did general H^n. The combinatorics was fiddly but it worked out.

[Adam Topaz]

One approach is to use the homotopy groups of BGL^+, but of course that would require homotopy groups, and the classifying space construction, and the plus construction, and probably 50 other things that are missing... (I'm also thinking of the algebraic context)

[Justus Springer]

Johan Commelin said:

Justus Springer Welcome btw :hello: . Which university are you at?

I'm from Tübingen, Germany

[Johan Commelin]

Cool, I'm in Freiburg. Several people in Karlsruhe use (or develop!) Lean

[Justus Springer]

Adam Topaz said:

One approach is to use the homotopy groups of BGL^+, but of course that would require homotopy groups, and the classifying space construction, and the plus construction, and probably 50 other things that are missing... (I'm also thinking of the algebraic context)

Right, that's Quillens plus-construction. I've seen a lot of homotopy theory in the HoTT library for lean 2, like higher homotopy groups, the suspension functor, hopf fibration... All of which would be necessary for K-theory I suppose. I haven't found homotopy theory in mathlib, which surprised be as it seems like a pretty elementary notion.

[Johan Commelin]

It is elementary in HoTT, but I wouldn't call it very elementary in "ordinary" foundations.

[Justus Springer]

Btw I'm no expert on K-theory, but will have some free time in the upcoming months and I'm planning to get my hands dirty with lean. I'm just brainstorming about a cool project I could take on :smile:

[Johan Commelin]

Given that mathlib has roughly 50% of an undergrad curriculum.... there are still lots of holes.

[Adam Topaz]

There's another approach to K-theory, which is more natural, i.e. as some higher (in the sense of higher algebra) version of the groupification of a monoid. This could be another approach to formalizing K-theory, but it would need to be done carefully, otherwise there will be universe issues.

[Justus Springer]

Johan Commelin said:

Cool, I'm in Freiburg. Several people in Karlsruhe use (or develop!) Lean

Nice!