Structure of ℤ_[p]ˣ

Stream: Is there code for X?

[Jz Pan]

Do we have any results related to structure of $\Z_p^\times$ in mathlib?

[Jz Pan]

I think I probably need the following:

1. $\Z_p^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}\times(1+2p\Z_p)$, p-adic logarithm, Teichmuller character, etc.
2. classification of closed subgroups of $\Z_p^\times$, particularly, an infinite closed subgroup of $\Z_p^\times$ is open and has an open subgroup isomorphic to $\Z_p$ (or I should say its quotient by torsion subgroup is isomorphic to $\Z_p$, in this way I can construct cyclotomic $\Z_p$-extension)

The proof of 2 should depends on 1 and classification of closed subgroups of $\Z_p$ (which is done in https://github.com/acmepjz/lean-iwasawa/blob/67c0b6b7e5e1bad600438db15cc6989ca8b8ee4b/Iwasawalib/NumberTheory/Padics/HasBasis.lean#L139).

[Jz Pan]

BTW we don't have PowerSeries.log but only docs#PowerSeries.exp

[Jz Pan]

A loogle search reveals that there are almost nothing mentioning $\Z_p^\times$ besides cyclotomic character

[Kevin Buzzard]

We need the local isomorphism between a char zero nonarch local field and its units for the class field theory project

[Yakov Pechersky]

Do you get the first from the more general statement docs#IsDiscreteValuationRing.eq_unit_mul_pow_irreducible ?

[Jz Pan]

Yakov Pechersky said:

Do you get the first from the more general statement docs#IsDiscreteValuationRing.eq_unit_mul_pow_irreducible ?

No, the result you mentioned gives $\Z_p\setminus\{0\}=\Z_p^\times\times p^\N$

[Jz Pan]

Let me clarify the map $\Z_p^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}\times(1+2p\Z_p)$.

Firstly we have $\omega:\Z_p^\times\twoheadrightarrow(\Z/q\Z)^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}$ here q = 4 if p = 2 and q = p otherwise.
When p is odd, the map $(\Z/q\Z)^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}$ can be obtained by docs#WittVector.teichmuller.
When p = 2 it can be defined directly. (Or I can use docs#hensels_lemma ? It looks very specific...)

The map $\langle\ \rangle:\Z_p^\times\twoheadrightarrow(1+2p\Z_p)$ is $a\mapsto a/\omega(a)$.

[Jz Pan]

Seems that I can't use PowerSeries.eval on p-adic exp and log since they are Qp-valued... cc @Antoine Chambert-Loir do you have any ideas on that? Perhaps I should use exp(p*x) and log(1+2*p*x) instead, I think they have Zp-valued coefficients?

[Junyan Xu]

Can you first show exp and log give an isomorphism between their balls of convergence, and then identify the balls with $1+2p\mathbb{Z}_p$ and $q\mathbb{Z}_p$ respectively?

[Junyan Xu]

Jz Pan said:

Let me clarify the map $\Z_p^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}\times(1+2p\Z_p)$.

In general if you have an exact sequence $1\to A \to B \to C\to 1$, then a left inverse to $B\to C$ induces an isomorphism $B\cong A\times C$. Here $B =\mathbb{Z}_p^\times$, $A = 1 +2p\mathbb{Z}_p$ and $C=(\mathbb{Z}/q\mathbb{Z})^\times$ and $\omega$ is the left inverse. Since $A$ is torsion-free (being isomorphic to the additive group of $\mathbb{Z}_p$), $C$ is the torsion part of $A$.

[Jz Pan]

Junyan Xu said:

Can you first show exp and log give an isomorphism between their balls of convergence, and then identify the balls with $1+2p\mathbb{Z}_p$ and $q\mathbb{Z}_p$ respectively?

Oh OK. I think this have to be some sooner or later...

[Jz Pan]

Junyan Xu said:

In general if you have an exact sequence $1\to A \to B \to C\to 1$

But we don't have multiplicative version of Exact in mathlib yet...

[Antoine Chambert-Loir]

To answer your question of yesterday: what we did with @María Inés de Frutos Fernández is evaluation of power series in algebraic settings where there are rings and ideals all over the place. That would in particular handle evaluation of power series in $\mathbf Z_p$ at points of $p\mathbf Z_p$.

[Antoine Chambert-Loir]

What you need is of a different nature, using radius of convergence, etc. and the model rather would be docs#FormalMultilinearSeries.radius

[Yakov Pechersky]

So on its own, there's no way to discuss evaluation of PowerSeries.exp or the to-be-defined log, on p adics, because the coefficients are in Q_p? And if one did connect PowerSeries evaluation to evaluation of FormalMultilinearSeries, how would one state the relationship between a radius-rescaled exp and the original exp?

[Junyan Xu]

It's probably the case that the mutually inverse power series $(e^{qX}-1)/q$ and $\log(1+qX)/q$ have coefficients in $\mathbb{Z}_p$ ...

[Yakov Pechersky]

That's fair. Still, how would even state the relationship between $(e^{qX} - 1) / q$ and $e^X$ as power series, either formally or their evaluation?

[Junyan Xu]

Apparently there's PowerSeries.rescale but nothing about it's evals ...

[Yakov Pechersky]

I'll look into maybe phrasing a PowerSeries -> FormalMultilinearSeries and one could discuss relationships using over that map.

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

Junyan Xu said:

Apparently there's PowerSeries.rescale but nothing about it's evals ...

Maybe MvPowerSeries.rescale_eq_subst and MvPowerSeries.eval₂_subst would be helpful.

[Jz Pan]

Yakov Pechersky said:

That's fair. Still, how would even state the relationship between $(e^{qX} - 1) / q$ and $e^X$ as power series, either formally or their evaluation?

In my application, $(e^{qX} - 1) / q$ seems to be enough and actually I don't use $e^X$.

[Jz Pan]

In fact what I'm thinking is that it's best if we have exp and log for a formal group (in our application it's exp and log for the formal multiplicative group $\widehat{\mathbb{G}}_m$).

[Jz Pan]

... or maybe we can cheat by proving isomorphism $\ker\big((\Z/qp^n\Z)^\times\to(\Z/q\Z)^\times\big)\xrightarrow\sim\Z/p^n\Z$ then taking inverse limit (fake, in the Lean proof we actually take Cauchy sequence)?

[Junyan Xu]

If you have the appetite to follow Serre's proof (p.17 of A Course in Arithmetic):
image.png

[Yakov Pechersky]

For reference, this is from Gouvea
Screenshot_20250626_090135_Drive.jpg
Screenshot_20250626_090338_Drive.jpg

[Junyan Xu]

But we don't have multiplicative version of Exact in mathlib yet...

You can work with $A$ being the kernel of $B \to C$

[Antoine Chambert-Loir]

By the way, an almost merged PR computes the order of $1+p$ mod $p^n$.

[Jz Pan]

Antoine Chambert-Loir said:

By the way, an almost merged PR computes the order of $1+p$ mod $p^n$.

I see, the PR concerning whether $(\Z/n\Z)^\times$ is cyclic

[Antoine Chambert-Loir]

Right. #26020.
And it also contains the result for $p=2$.

[Kevin Buzzard]

I am hoping that the general theory of p-adic exp and log (for finite extensions of Qp not just Qp) will be formalised like this: (1) exp log = id and log exp = id for real numbers (2) exp log = id and log exp = id as abstract power series with rational coefficients (3) exp log = id and log exp = id for p-adic fields. The reason I think this is the correct route is that exactly the same strategy (deducing results about the p-adic numbers for results about the reals) can be used to prove the existence of the Tate curve (a family of elliptic curves over p-adic fields) from classical results about the Weierstrass P-function (I wrote down the corresponding power series identity in a mathoverflow post a year or two ago)

[Kevin Buzzard]

We need exp and log for general char 0 local fields, for class field theory, and we need the elliptic curve variant for FLT. A crucial fact is that exp and log commute with inclusions between p-adic fields because this is what gives you the claim that the local isomorphism is Galois equivariant. This is why working over $\mathbb{Q}_p$ alone isn't enough. The entire thing should be set up for characteristic zero nonarchimedean normed fields.

[Jz Pan]

Kevin Buzzard said:

and we need the elliptic curve variant for FLT

So ideally we should do exp and log for formal groups

[Jz Pan]

Do you think following Chapter 4 of Silverman's GTM106 is a good idea?

[Jz Pan]

exp log = id and log exp = id

I think it should be easy to state this for formal groups, since these two power series have no constant terms hence this is formal composition which is defined for any rings without requiring topology.

[Kevin Buzzard]

I think that @María Inés de Frutos Fernández was thinking about formal groups at some point, maybe they can say something concrete

[Antoine Chambert-Loir]

The work she and I did on power series will allow to define them and to start proving results, as soon as you evaluate points in topologically nil-ideals, but you will need coefficients to live in the base ring, which is not the case for exp and log. Otherwise all formal groups would be isomorphic to Ga (and to Gm).

[Jz Pan]

Cool.

For the structure of $\Z_p^\times$ I think I can do it by cheating (hopefully without any exp and log).

But sooner or later maybe I'll look at formal groups. At least it's needed in arithmetic of elliptic curves, e.g. Neron-Ogg-Shafarevich criterion (if I remembered correctly).

[Kevin Buzzard]

Formal groups also tell you that there's a finite index subgroup of the points of an elliptic curve over a p-adic field which is torsion-free and hence that the local torsion is finite (and hence so is the global torsion over a number field). It also tells you that coprime to p part of global torsion embeds into points of the reduced curve mod p

[Antoine Chambert-Loir]

This remark is slightly off topic, but I believe one shouldn't think of this result as belonging to the theory of formal groups, but rather on the theory of $p$-adic Lie groups: this has to do with convergence of the logarithm/exponential maps.

[Jz Pan]

Junyan Xu said:

Jz Pan said:

Let me clarify the map $\Z_p^\times\xrightarrow\sim(\Z_p^\times)_{\mathrm{tors}}\times(1+2p\Z_p)$.

In general if you have an exact sequence $1\to A \to B \to C\to 1$, then a left inverse to $B\to C$ induces an isomorphism $B\cong A\times C$. Here $B =\mathbb{Z}_p^\times$, $A = 1 +2p\mathbb{Z}_p$ and $C=(\mathbb{Z}/q\mathbb{Z})^\times$ and $\omega$ is the left inverse. Since $A$ is torsion-free (being isomorphic to the additive group of $\mathbb{Z}_p$), $C$ is the torsion part of $A$.

OK now I formalized the natural continuous isomorphism $\Z_p^\times\cong(1+p^n\Z_p)\times\mu_{\varphi(p^n)}$ where n = 2 if p = 2, n = 1 otherwise. See https://github.com/acmepjz/lean-iwasawa/blob/08e3c0cf907175357163aa115e064274ae75866f/Iwasawalib/NumberTheory/Padics/Units.lean#L348.

To do this, the Teichmuller map $(\Z/p^n\Z)^\times\to\Z_p^\times$ is defined, which is injective (proved) with image $\mu_{\varphi(p^n)}$ (to be shown). This is the first time docs#hensels_lemma is used (it was only imported by Mathlib).

Next project is prove that $1+p^n\Z_p$ is isomorphic to $\Z_p$, in particular, it does not have nontrivial roots of unity, so $\mu_{\varphi(p^n)}$ is the only roots of unity in $\Z_p$.

[Jz Pan]

(Or maybe we should use https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Henselian.html instead?)

[Junyan Xu]

Maybe you can use Polynomial.card_nthRoots or docs#isCyclic_of_subgroup_isDomain etc.

[Jz Pan]

I've constructed the map $\Z_p\to 1+p^n\Z_p$, $x\mapsto(1+p^n)^x$ and proved that it's bijective, and maps addition to multiplication.

The last step is to prove that it's continuous.

Unfortunately the full codes are near 1000 lines :man_facepalming:

[Junyan Xu]

Did you use UniformContinuous.extend in the construction? You'd only need to prove it's uniformly continuous on Z by Dense.uniformContinuous_extend.

[Jz Pan]

Junyan Xu said:

Did you use UniformContinuous.extend in the construction? You'd only need to prove it's uniformly continuous on Z by Dense.uniformContinuous_extend.

Not yet. I proved that $\N\to\N$, $k\mapsto(1+p^n)^{x\bmod p^k}$ form a Cauchy sequence hence gives an element in $\Z_p$...

Extending a continuous function on a dense subset seems to be a good idea...

[Jz Pan]

OK the https://github.com/acmepjz/lean-iwasawa/blob/7c4da1d85dfab297a12e1ac30101254f9581cc5a/Iwasawalib/NumberTheory/Padics/Units.lean#L884 is sorry-free:

open equivTorsionfreeUnits in
/-- The continuous group isomorphism `(ℤₚ, +) ≃ (1 + pᵏℤₚ, *)` by sending `x` to the limit of
`(1 + pᵏ) ^ (x mod pⁿ)` as `n → ∞`, where `k = 2` if `p = 2`, and `k = 1` otherwise. -/
noncomputable def equivTorsionfreeUnits : Multiplicative ℤ_[p] ≃ₜ* torsionfreeUnits p :=

The continuity is the corollary of:

theorem toFun_mem_principalUnits_iff (x : ℤ_[p]) :
    (isUnit_toFun p x).unit ∈ principalUnits p (n + torsionfreeUnitsExponent p) ↔
      x ∈ Ideal.span {(p ^ n : ℤ_[p])} := by

[Jz Pan]

I'm going back to working on cyclotomic $\Z_p$ extension now.

Do you think the results on the structure of $\Z_p^\times$ should go to mathlib? Or should we add a more general version on $\mathcal{O}_K^\times$ for K a (finite) extension of $\mathbb{Q}_p$?

[Kenny Lau]

why not both

[Riccardo Brasca]

We surely want both versions!

[Kevin Buzzard]

Do we have a good way of saying "finite extension of Q_p" that would apply to eg the completion of a number field at a finite place?

[Jz Pan]

I think we have results on $\mathcal{O}_K^\times$ whenever $K$ is a mixed-characteristic CDVF? Perhaps we also have results on $\mathcal{O}_{\mathbb{C}_p}^\times$?

[Jz Pan]

So we don't necessarily require that K is a finite extension.

[Jz Pan]

Do we have some standard textbook reference? I'm checking Local Fields and Their Extensions by Fesenko and Vostokov now.

[Jz Pan]

Chapter I. Complete Discrete Valuation Fields
...
6. The Group of Principal Units as a $\Z_p$-module

OK this is what I want to find

Chapter VI. The Group of Units of Local Number Fields
1. Formal Power Series
2. The Artin–Hasse–Shafarevich Map
3. Series Associated to Roots
4. Primary Elements
5. The Shafarevich Basis

Wait, it seems not so easy... ?

[Kevin Buzzard]

For finite extensions of Q_p equipped with a norm normalised so that $|p|=e$ the statements are that exp and log are inverse bijections between the open disc centre 0 radius e^{1/(p-1)} and the open disc centre 1 radius e^{1/(p-1)}, and that these maps commute with morphisms of finite extensions of Q_p (which don't change $e$, say). And these proofs aren't hard. It's when you start worrying about char p that things get a bit hairier.

[Paul Lezeau]

Yakov Pechersky said:

I'll look into maybe phrasing a PowerSeries -> FormalMultilinearSeries and one could discuss relationships using over that map.

@Yakov Pechersky Did you ever get around to doing this? @Xavier Généreux and I have made a start at it today (I just saw the message above now!) but haven't gotten very far yet

[Yakov Pechersky]

No -- haven't built the API there, I'd been prioritizing the ValuativeRel refactor. My contribution on this is just to make PowerSeries.eval available for Z_p coefficient power series (#24627), which doesn't help with exp.