Z-hat

Stream: Is there code for X?

[Kevin Buzzard]

The profinite completion $\widehat{\Z}$ of $\Z$ is a basic type (so should be in core really). Do we have it in mathlib? It's a topological ring, equal to the projective limit of $\Z/N\Z$ over the positive naturals. It's really essential that the limit is over the positive naturals; taking it over all the naturals would just leave you with $\Z$ again.

One definition of the finite adeles of a number field $K$ is $K\otimes_{\Z}\widehat{\Z}$ (this is a trick I learnt from Maria Ines), and one definition of the infinite adeles of a number field is $K\otimes_{\mathbb{Q}}\mathbb{R}$, so you can see that both constructions are in some sense a completion of the number field, the first nonarchimedean and the second archimedean. If we had a $\widehat{\Z}$ we'd have all the ingredients for this definition.

[Adam Topaz]

You could just take the product of all the $\Z_p$’s.

[Jz Pan]

More generally, you can define the profinite completion $\widehat{G}$ of an abelian group $G$ by the same way. Seems that it doesn't generalize to non-commutative groups.

[Filippo A. E. Nuccio]

I agree that $\mathbb{A}_K^f=\mathbb{A}_{\mathbb{Q}}^f\otimes\hat{\mathbb{Z}}$ but I do not think this would be the "right" definition in mathlib, mainly because it does not generalise to function fields and it puts a lot of emphasis on the $\mathbb{Z}$-structure of $K$ through the ScalarTower $\mathbb{Z}\to\mathbb{Q}\to K$. Also, one would immediately run into nasty commutativity issues of the form $\mathbb{A}_L^f=\mathbb{A}_K^f\otimes L=K\otimes\hat{\mathbb{Z}}\otimes L=L\otimes\hat{\mathbb{Z}}$... But since your question was purely about $\hat{\mathbb{Z}}$ this is probably not very relevant.

[Jz Pan]

Filippo A. E. Nuccio said:

one would immediately run into nasty commutativity issues

Maybe it's better to write $\widehat{\mathbb{Z}}$ on the left...

[Kevin Buzzard]

I write L on the left!

[Adam Topaz]

Jz Pan said:

More generally, you can define the profinite completion $\widehat{G}$ of an abelian group $G$ by the same way. Seems that it doesn't generalize to non-commutative groups.

The profinite completion is perfectly well-defined for noncommutative groups. You just take the limit over all finite quotients. In the commutative case, i.e. when $A$ is an abelian group you can talk about the adic completion which is the limit of $A/nA$ as $n$ varies, but this is a separate concept. In the case of $A = \Z$ the adic and profinite completions agree.

[Adam Topaz]

I think adic completions should be added to mathlib, but that they should be done in a suitable level of generality. One option could be to define so-called "truncation sets" (see this for example) and define an adic completion for any truncation set $S$.

[Adam Topaz]

Thus if $S = \{1,p,p^2,\ldots\}$, you would get the $p$-adic completion, and when $S = \N+$ you get the full adic completion

[Adam Topaz]

(Truncation sets also show up in the theory of big Witt vectors, so it makes sense to have these anyway IMO!)

[Jz Pan]

Adam Topaz said:

The profinite completion is perfectly well-defined for noncommutative groups. You just take the limit over all finite quotients.

I see. But what about a group which has no non-trivial finite quotients (e.g. an infinite "simple group"?)

In the commutative case, i.e. when $A$ is an abelian group you can talk about the adic completion which is the limit of $A/nA$ as $n$ varies, but this is a separate concept. In the case of $A = \Z$ the adic and profinite completions agree.

Oh I see. I missed that problem. So for $\mathbb{Z}[X]$ these two don't agree?

[Johan Commelin]

Right. The profinite completion can be trivial. The map from G to the completion does not have to be injective.

[Mitchell Lee]

Adic completions are already in mathlib: you equip a ring with the adic topology (docs#Ideal.adicTopology) and then take the completion (docs#UniformSpace.Completion), which comes with a ring structure (docs#UniformSpace.Completion.ring). In fact, I have a PR which proves that it's even a nonarchimedean ring (#12669).

I don't think it's been proved in mathlib that the $I$-adic completion of $R$ is the limit of the quotients $R / I^n$, but this can be stated using docs#CategoryTheory.Limits.IsLimit rather than taken as the definition.

To get $\hat{\mathbb{Z}}$, you start with a different linear topology: the one generated by the cosets of nonzero ideals. I think @Antoine Chambert-Loir and @María Inés de Frutos Fernández were discussing adding linearly topologized rings to mathlib.

[Mitchell Lee]

Oh, in fact, adic completions are in mathlib twice. You can either use docs#UniformSpace.Completion with the adic topology, or you can use docs#AdicCompletion. I'm not sure whether there is any mathematical difference between these two or why you would want to use one over the other.

[Johan Commelin]

The docstring of docs#AdicCompletion says

The completion of a module with respect to an ideal. This is not necessarily Hausdorff. In fact, this is only complete if the ideal is finitely generated.

Also, it doesn't assume a preexisting uniform structure on the ring. So I guess there is both a difference in maths and in intended API.

[Antoine Chambert-Loir]

Yeah, “adic completion” is really a poor name, but that's too late to get a new one (“adiction” ?) On the other hand, any ideal gives rise to a adic-uniform structure. Compared to paper-math, mathlib's docs#UniformRing implicitly allow for more general ones.

[Mitchell Lee]

This is maybe a stupid question, but can you give an example where the result of docs#AdicCompletion isn't Hausdorff?

[Kevin Buzzard]

(deleted)

[Antoine Chambert-Loir]

The paper by Amnon Yekutieli (2011), “On Flatness and Completion for Infinitely Generated Modules over Noetherian Rings”, Communications in Algebra, 39:11, 4221-4245, seems to prove that if $R$ is a ring, $I$ an ideal of $R$ and $M$ is any $R$-module, then the $I$-adic completion of $M$, $\varprojlim M/I^n M$ is Hausdorff (Corollary 1.7).

[Antoine Chambert-Loir]

The standard example (Bourbaki, Commutative Algebra, chapter III, §2, exercise 12) proves something else: if $R=K[T_1,\dots]$ is the ring of polynomials in infinitely many indeterminates, $M=\langle T_1,\dots\rangle$ is its maximal ideal of polynomials vanishing at 0, then the $M$-adic completion $\widehat R$ identifies with the ring of power series in $T_1,\dots$ of which every homogeneous part is a polynomial. This ring is a local ring, but its maximal ideal $\widehat M$ (these power series without constant term) is not the closure of $M\cdot \widehat R$, as the example of $f=\sum T_n^n$ shows. As a consequence, the topology of $\widehat R$ is not $M$-adically complete. In fact it is even not $\widehat M$-adically complete. The example in Bourbaki only addresses the cases where $K$ is a finite field, but according to the Stacks Project, Tag 05JA and unpublished note by De Smit and Lenstra, this should hold in general. (The ideal $\widehat M^2$ is not the kernel of the canonical map $\widehat R \to R/M^2$.)