ZHat

Stream: Is there code for X?

[Kevin Buzzard]

In another conversation #Is there code for X? > Properties of prime subfield @ 💬 , David Loeffler and I were agreeing that mathlib should have a basic type ZHat : Type. This is a commutative topological ring defined mathematically as the projective limit of $\Z/n\Z$ as $n$ ranges over the positive integers ordered by divisibility. This type is a universal nonarchimedean completion of the integers, just as the reals are the archimedean completion of the rationals.

In FLT we have been using this definition for a year now; it has been battle-tested there and seems to be working fine. The actual definition of ZHat is an implementation detail of course; another way we could define it would be as a subring of the finite adeles of the rationals, which would I guess make it much easier to relate to the finite adeles of the rationals, but would have the disadvantage that there would be HeightOneSpectrum (𝓞 ℚ) everywhere, which would make basic API building a nightmare. With my proposed definition it's going to be easy relating this to any kind of completion of the integers.

I am never quite sure how to approach decisions such as this. Would mathlib prefer a 100-line PR with the definition and a promise that it works, or a 300-plus-line PR proving that that it works? Anyway, before even embarking on either I thought I'd raise the question explicitly here.

[Edison Xie]

Do we now have IsInverseLimit and IsDirectLimit now?

[Johan Commelin]

I would go for the 300-line version. Eg would be nice to get an isom with product of Z_[p]s.

[Adam Topaz]

I think the type of ZHat should be Set Nat.Primes -> Type, sending a set of primes S to the S-adic completion of Z.

[David Michael Roberts]

As some kind of Ind-ring?

[David Michael Roberts]

(deleted)

[Scott Carnahan]

We could also have an object of the same type as Adam Topaz’s suggestion, but instead sending S to ZHat tensor S-integers, i.e., inverting the primes in S.

[Kevin Buzzard]

This would also give QHat := $\widehat{\Z}\otimes\mathbb{Q}$, which is another "basic type" IMO.