Contribute a project on ramification theory

Stream: new members

[Jiang Jiedong]

Hi everyone!

As I notice that there is still little written about the theory of ramification of valuations in mathlib, my friends and I want to make some contribution to mathlib about this topic, in lean4. (also serving for a further goal of proving properties about ℂ_p ) Is there some project similar already in progress? If so, should I talk with someone to see if we could collaborate? I know that @María Inés de Frutos Fernández has made some progress on local fields. :tada:

A reference I choose is the second chapter of Neukirch's Algebraic Number Theory. Maybe someone has some better material in mind?

I haven't contributed to mathlib before, but I really hope to make contributions to mathlib this time. Is this a good topic that mathlib4 will record? Is there some written style guidance of mathlib I need to learn, or someone I need to discuss with before I start on working on the project? Or should I first write then gradually modify the project to meet the standard of mathlib? I really know nothing about how to contribute to mathlib. :thinking:

Any suggestions is welcome! Thanks in advance!

[Ruben Van de Velde]

If you want to submit to mathlib, I think it will be best to submit additions for review as soon as possible, rather than waiting until you've got a lot of code. That way you'll learn from the reviews sooner and you'll probably find it easier to get reviews for small changes

[Johan Commelin]

@Jiang Jiedong https://www.youtube.com/watch?v=Bnc8w9lxe8A&pp=ygUiY3JlYXRpbmcgYSBwdWxsIHJlcXVlc3QgdG8gbWF0aGxpYg%3D%3D is a video that explains the technical aspects of contributing to mathlib.

[Johan Commelin]

https://leanprover-community.github.io/contribute/index.html contains links to style guides etc. As you can see from the warning at the top of the page, this website is still about lean 3. We hope to transition the website to lean 4 asap.

[Johan Commelin]

As Ruben explained, we recommend that a first PR contains < 300 lines, just to get familiar with the process etc...

[Kevin Buzzard]

We have sum of e_i f_i is n and that theorem should be applicable to local fields. I think that defining the p-adic and mod p cyclotomic characters (on the absolute Galois group of any field) would be a nice place to start. We also need decomposition and inertia and higher ramification groups for finite extensions with the lower numbering, that's something else feasible I think

[Kevin Buzzard]

At some point a discussion will need to be had about what Frob pi will mean. I am coming around to the idea that even if the extension is ramified, Frob should just be a random element of the Galois group

[Jiang Jiedong]

@Ruben Van de Velde @Johan Commelin Thanks! Then I shall try to make a first pull request in next week in order get familiar with the flow chart and get fast feedbacks.

[Jiang Jiedong]

Kevin Buzzard said:

We have sum of e_i f_i is n and that theorem should be applicable to local fields. I think that defining the p-adic and mod p cyclotomic characters (on the absolute Galois group of any field) would be a nice place to start. We also need decomposition and inertia and higher ramification groups for finite extensions with the lower numbering, that's something else feasible I think

Yes, decomposition and inertia and higher ramification groups is exact what I want to do. Thank you for your advice! I believe p-adic and mod p cyclotomic characters is a good choice for my first PR.

[Jiang Jiedong]

By the way, I'm still experiencing some difficulties in finding theorems like sum of e_i f_i is n in mathlib. Is there some convenient way (maybe some searching tools or some chart) for looking up in the mathlib?

[Johan Commelin]

@Jiang Jiedong Here's what I would do: I search through mathlib for files containing the string "ramif". That gives me this list

docs/references.bib
Mathlib/NumberTheory/RamificationInertia.lean
Mathlib/RingTheory/Valuation/RamificationGroup.lean

Those last two files both look interesting.

I open the first file, and scan through the documentation at the top of the file. It says:

The main theorem `Ideal.sum_ramification_inertia` states that for all coprime `P` lying over `p`,
`Σ P, ramification_idx f p P * inertia_deg f p P` equals the degree of the field extension
`Frac(S) : Frac(R)`.

[Johan Commelin]

Of course this doesn't always work. But usually a text search is quite helpful

[Johan Commelin]

If text search doesn't get you anywhere, don't hesitate to ask in the stream #Is there code for X?

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

Hi Jiang! @Filippo A. E. Nuccio and I are working on local fields and ramification is one of the next goals we had in mind. We should coordinate to avoid duplicating work.