Class Field Theory

Stream: Is there code for X?

[Steven Rossi]

Is there really mathlib stuff for class field theory? It looks like there’s a few things for basic number fields, unit groups, etc but many other parts don’t seem flushed out.

[Riccardo Brasca]

We don't have class field theory in mathlib, but there are several people working on it, or on closely related problems. Do you need it for a specific goal or are you interested in proving it?

[Steven Rossi]

Im interested in proving it if it doesn’t exist. Most of what I do is computational CFT, so it’d be nice to have in mathlib.

[Riccardo Brasca]

One of the main persons to talk to is @María Inés de Frutos Fernández

[Steven Rossi]

Great thanks, I just saw her papers on the topic, definitely what I’m looking for

[María Inés de Frutos Fernández]

I am working with @Filippo A. E. Nuccio towards a formalization of local class field theory. So far, we have formalized some of the fundamental theory of local fields (and more generally, of fields complete with respect to a discrete valuation). Our work so far is available at this repository. In previous work, I also formalized the ring of adeles (much of that formalization project is now available in mathlib, see for instance docs#DedekindDomain.finiteAdeleRing).

[Kevin Buzzard]

Someone called Richard Hill, who is not on this Zulip but is going to be teaching a lean course at UCL and is in contact with me, is interested in formalising the global aspects. Last time we talked about this he said he had given an elementary proof of the main results in his PhD thesis via a proof which used no analysis and reduced the question to Kummer theory. I think everything is in place to start formalising Kummer theory a la Birch's paper in Cassels-Froehlich.

[Kevin Buzzard]

In some sense we're working through Cassels-Froehlich (Anne Baanen and their team have done much of the local and global theory, Maria Ines has done adeles, Amelia Livingston has done group cohomology and profinite cohomology, the FLT-regular crowd have done cyclotomic fields, and IIRC Kummer theory is the next topic in the book.)

[Kevin Buzzard]

Not all of everything is done in the previous chapters but my gut feeling is that enough is done to do all the Kummer theory section in Birch's paper.

[Steven Rossi]

Ah well I don’t want to step on anybody’s toes for the global and local stuff, but I’ll definitely take a look at Birch’s paper

[Kevin Buzzard]

Believe me there is a huge amount to do before we get to class field theory, and it's not called stepping on anyone's toes, it's called collaboration :-)