AdicCompletion vs HeightOneSpectrum.adicCompletion

Stream: mathlib4

[Yaël Dillies]

In mathlib we have two things called "adic completion": docs#AdicCompletion and docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion. I seem to understand that those are mathematically different objects, but I haven't been able to assert this by reading the docs. Could we please

1. Clarify whether those are mathematically different or not (and indicate so in the docs!).
2. If not, unify them.
3. If so, move AdicCompletion to a namespace.

[Yaël Dillies]

Context is that I was working on FLT#230 and accidentally generalised the wrong Algebra instance

[Yaël Dillies]

(nothing bad, to be clear, I just need to redo the same thing a second time to actually close FLT#230)

[David Loeffler]

They are closely related, but neither is quite a special case of the other.

The relation is that if R, K, v are as in docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion, the ring docs#IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (i.e. the subring of docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion consisting of stuff with valuation ≤ 1), is canonically isomorphic to the docs#AdicCompletion of R, as a module over itself, wrt the prime ideal I corresponding to the place v.

[Adam Topaz]

It probably wouldn’t hurt to move docs#AdicCompletion to the Ideal namespace.

[Adam Topaz]

This is really a consequence of imprecise naming in informal math. We say that $\mathbb{Q}_p$ is the $p$-adic completion of $\mathbb{Q}$ and $\Z_p$ is the $p$-adic (or $(p)$-adic) completion of $\Z$. But the $(p)$-adic completion of $\mathbb{Q}$ is the trivial ring :-/

[Christian Merten]

Note that docs#Padic is defined neither via docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion nor via docs#AdicCompletion but via docs#CauSeq.Completion.Cauchy.

[Yaël Dillies]

David Loeffler said:

The relation is that if R, K, v are as [...]

Ah great! I was confused why AdicCompletion K (span {v}) wasn't literally the same as v.adicCompletion K. The answer is that one is the fraction field of the other

[Johan Commelin]

And as David and Adam explain, you even need R instead of K in the first expr. So yeah, it's confusing.

[Yaël Dillies]

So one is the adic completion of a ring and the other is the adic completion of a field. Maybe we could call them RingAdicCompletion and FieldAdicCompletion? It's not much longer and clearly disambiguates them

[Filippo A. E. Nuccio]

Christian Merten said:

Note that docs#Padic is defined neither via docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion nor via docs#AdicCompletion but via docs#CauSeq.Completion.Cauchy.

Note that in our work with @María Inés de Frutos Fernández we prove that they are isomorphic.

[Filippo A. E. Nuccio]

Concerning the whole discussion, I think that one point to keep in mind is that the AdicCompletion can be defined basically with no assumption on the ring, whereas IsDedekindDomain.HeightOneSpectrum.adicCompletion only makes sense for Dedekind Domains. I think that given the applications it makes sense to treat adic completions of Dedekind Domains with a preferred eye (there will be more API in that setting) and using only namespaces to distinguish this special case might be misleading. I guess this is what motivated @María Inés de Frutos Fernández in the first place, but I let here intervene here.

[Filippo A. E. Nuccio]

Concerning the Ring vs Field confusion, I agree it is not great but one advantage of the current design (for Dedekind domains) is that it forces one to work with the completion of the field, and to look at the integers as the unit ball, that is isomorphic but not defeq to the completion of the Dedekind domain. If we have both definitions, both things would appear somewhat randomly and I believe that the library would soon become a mess.