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.

[Jz Pan]

I have a misc math problem: in our blueprint the following property for a Noetherian ring A is considered

it's called "height one localizations are PID", if for any finitely mane height one primes $\mathfrak{p}_1,\cdots,\mathfrak{p}_n$ of A, the localization $(A\setminus(\mathfrak{p}_1\cup\cdots\cup\mathfrak{p}_n))^{-1}A$ is a PID.

If such condition is satisfied, then being pseudo-isomorphic has nicer properties, and structure theorem of finite generated torsion module up to pseudo-isomorphism holds.

It's known that if A is a domain, then this is equivalent to that for any height one prime $\mathfrak{p}$ of A, $A_{\mathfrak{p}}$ is a PID (because a semilocal domain is PID if its localization at all maximal ideals are PID).

But I don't know if there are interesting cases in Iwasawa theory that the structure theorem holds but A is not a domain? Is $\Z_p[[\mathrm{Gal}(\mathbb{Q}(\mu_{Np^\infty})/\mathbb{Q})]]$ an example? (Some trivial example for such non-domain A could be a finite product of fields? In this case it does not have height one primes at all.)

If there are no such examples, then I think I may add IsDomain A as a prerequisite of the definition "height one localizations are PID" and make it simpler.

[Kevin Buzzard]

How close is "all A_P is PID" to "A is a UFD"?

[Jz Pan]

Kevin Buzzard said:

How close is "all A_P is PID" to "A is a UFD"?

For dimension one case, "all A_P is PID" is true for Dedekind domains which are not UFD in general.

[Antoine Chambert-Loir]

Kevin Buzzard said:

How close is "all A_P is PID" to "A is a UFD"?

Isn't this call the class group?