Discussion on formalization of Iwasawa Theory in Lean

Stream: maths

[Jz Pan]

Here is the discussion thread on the formalization of some basic concepts of Iwasawa Theory in Lean.

It's a tentative project in Academy of Mathematics and Systems Science, Chinese Academy of Sciences.

I've setup a basic WIP blueprint website at https://acmepjz.github.io/lean-iwasawa.

The first goal of this project is formalize the proof (to some extent as much as possible) of the following result of Iwasawa on growth of class groups in $\mathbb{Z}_p$-extension.
Due to the funding period, this is expect to be concluded in the end of this year (2025).

Let $K$ be a number field, $p$ be a prime, $K_{\infty}/K$ be a $\mathbb{Z}_p$-extension.
Then there exists $\lambda,\mu,\nu$ such that for any sufficiently large $n$, $\mathrm{ord}_p(\mathrm{Cl}(K_n))=\mu p^n+\lambda n+\nu$.

The proof of it requires certain amount of commutative algebra and algebraic number theory (more precisely, global class field theory).

The next goal is a longer term goal, which is to formalize the proof of cyclotomic Iwasawa Main Conjecture which relates class groups of cyclotomic $\mathbb{Z}_p$-extensions to Kubota-Leopoldt $p$-adic $L$-functions.

In this thread I want to collect suggestions, opinions and feedbacks to the project, including but not limited to:

• Prerequisites of mathematics which may be used in this project, including those already in mathlib, or in PR, or in another repository, or in other ongoing projects. It's a bad idea to reinventing wheels.
• Suggestions for data structure designs.
• ......

Helps are welcome. Thanks in advance!

[Kevin Buzzard]

If any students want to come to the Clay Math summer school on formalising class field theory, I would encourage them to apply! https://www.claymath.org/events/formalizing-class-field-theory/ Closing date for registrations is just a few weeks away.

[Jz Pan]

Kevin Buzzard said:

If any students want to come to the Clay Math summer school on formalising class field theory, I would encourage them to apply!

Thank you! I'll keep in mind if there are students interested in it.

What I should do in our project is to keep the notation same as the formalizing class field theory project :).

[Jz Pan]

Filippo A. E. Nuccio said:

Jz Pan said:

BTW I'm trying IsZpExtension here https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/FieldTheory/ZpExtension/Basic.lean and I also defined a CommGroup instance. Clearly abelian extension is very useful in my application.

BTW, although a bit unrelated to this, I think we really need to set up the theory of multiple Zp extensions from the start indexed by a Fintype I and have an abbrev for the special case I=Unit as we do for polynomials.

Yes, it's certainly useful for Rubin's work of Iwasawa theory on imaginary quadratic fields. But in several variable case I think it's not clear how to define $\Gamma_n$ and $K_n$.

[Filippo A. E. Nuccio]

Not only Rubin's work, pretty much everything about modern (post 1970) Iwasawa theory needs to speak about multiple Zp extensions at a certain point: Leopoldt conjecture, maximal p-ramified extensions, Iwasawa th for elliptic curves and modular forms, etc. We can discuss things in Beijing in three weeks time, but if I have an idea about a nice definition for intermediate fields in between I'll mention it here. For the time being, I looked at your repo and I think all your preliminary results about uniqueness of subgrouos of given index and their topology will be useful, even in the rank-1 case.

[Jz Pan]

Filippo A. E. Nuccio said:

We can discuss things in Beijing in three weeks time

Sure.

but if I have an idea about a nice definition for intermediate fields in between I'll mention it here.

Sure. My plan is currently just define $K_n$ for [Unique I] case, and only define the subfield for several variable case when there are applications.

[Jz Pan]

I think we really need to set up the theory of multiple Zp extensions from the start indexed by a Fintype I and have an abbrev for the special case I=Unit

Now I defined IsMvZpExtension along with IsZpExtension. Since both of them are Props, if using Fintype I I still need a lemma that IsMvZpExtension depends on the cardinality of I. So I decide to make IsMvZpExtension accepts a natural number d as dimension for input, rather than a Fintype I. Hope it will not introduce troubles.

Meanwhile maybe we need a Type MvZpExtension which carries the data I as well as a fixed isomorphism of Galois group to Zp^d. For example in imaginary quadratic setting, we may choose (cyclotomic,anticyclotomic) directions, or $(\mathfrak{p},\overline{\mathfrak{p}})$ directions.

[Filippo A. E. Nuccio]

I think that the structure MvZpExtension would be useful, indeed. I am not sure yet whether having a general I rather than a Fin n is a problem, but I am not sure about the problem here: if you only define IsZpExtension as the existence of an iso between the Galois group and I -> Zp, can' you apply this def to Fin d when this makes your life easier?

[Jz Pan]

Filippo A. E. Nuccio said:

I am not sure yet whether having a general I rather than a Fin n is a problem

Suppose there are I and J with same cardinality. Then IsMvZpExtension p I K L if and only if IsMvZpExtension p J K L. But you need a lemma for this (although its proof is trivial).

If I just use a number, then it just becomes IsMvZpExtension p d K L where d = #I = #J. (Here # means Nat.card.)
And IsMvZpExtension p d K L = IsMvZpExtension p #I K L = IsMvZpExtension p #J K L is just by rw.

For the data version MvZpExtension p I K L it could have a lemma which implies IsMvZpExtension p #I K L.

[Filippo A. E. Nuccio]

Oh I see. Well l guess we can very well love with n instead of I.