Adeles over Q

Stream: FLT

[Bryan Wang]

(This is related to some of the previous discussion in #FLT > miniproject: adeles but I'm starting a new thread as that thread already seems overloaded)

Proving the cocompactness of the principal adeles of Q (FLT#258) turned out to be surprisingly more painful than I initially expected, because we don't have good ways to relate the FiniteAdeleRing API, in the case of K=ℚ, to the more 'down-to-earth' API for ℤ,ℚ, etc. However it turns out that one of the main results of chapter 5 of the blueprint, QHat.rat_join_zHat, is precisely the essential mathematical content we need for the proof of cocompactness. Therefore I wonder if we should relate QHat and FiniteAdeleRing, i.e. something like

/-- The equivalence between `FiniteAdeleRing (𝓞 ℚ) ℚ` and `QHat`. -/
def finiteAdeleRing_equiv_qHat : FiniteAdeleRing (𝓞 ℚ) ℚ ≃+ QHat := sorry

lemma principalSubgroup_equiv_ratsub :
    finiteAdeleRing_equiv_qHat '' (FiniteAdeleRing.principalSubgroup ℚ) = QHat.ratsub := sorry

lemma finiteIntegralAdeles_equiv_zHatsub :
    finiteAdeleRing_equiv_qHat '' (FiniteAdeleRing.finiteIntegralAdeles ℚ) = QHat.zHatsub := sorry

Of course, this is not exactly completely straightforward either, but it somehow seems to me to be a 'morally right' addition to the theory developed in chapter 5. With this, the proof of cocompactness becomes much more streamlined (the relevant PR is FLT#705).

[Bryan Wang]

I should also mention that a proof of such a statement is given in the wikipedia page for adele ring - albeit with the usual abuse of =!

[Ruben Van de Velde]

It does seem like having some API about FiniteAdeleRing in the specific case of Rat/Int would be useful. Rat.AdeleRing.zero_discrete looks like it's trying to push through this lack of API, for example. But if the other equivalence is more useful to you right now, it'd also make sense to work on that

[Kevin Buzzard]

Basically there is a design decision to be made here. For results like discreteness and cocompactness of $K$ in $\mathbb{A}_K$ you can either just prove it directly for all $K$ using standard facts about integer rings or you can prove it for $\mathbb{Q}$ using essentially nothing mathematically and then deduce it for general $K$ by using the fact that $\mathbb{A}_K=\mathbb{A}_{\mathbb{Q}}\otimes K$ algebraically and topologically. I went for the latter because I felt like it was an important result (for example it reduces the Langlands conjectures over a general number field to the Langlands conjectures for $\mathbb{Q}$ via restriction of scalars) and...well, here we are :-)

[Bryan Wang]

I agree with the choice to reduce to $\mathbb{Q}$, but then I was surprised at how much effort the proof was taking relative to its mathematical content, and it's probably because we're missing some API here. (For example we ideally want statements like the one here relating adicCompletion, which is used in FiniteAdeleRing, to Padic, but apparently this is not in mathlib yet.) However I then realised that we have an exactly mathematically equivalent statement QHat.rat_join_zHat proved in chapter 5 of the blueprint for QHat, and so now I think we should also try to relate QHat and FiniteAdeleRing.

[Kevin Buzzard]

Yeah chapter 5 was an experiment to see if this definition was more fun. One question is whether mathlib should have a bespoke ZHat type; the last time I asked it just degenerated into a conversation of how to define it without ever really deciding whether it should be there or not

[Kevin Buzzard]

The holiday season is over as far as I am concerned, and I am now finally back to spending several hours a day on FLT, so things are going to start moving again after a very slow 6 weeks or so.

It seems to me that this approach (define ZHat in a totally concrete way as is done in FLT, define QHat as Q tensor ZHat, prove stuff about QHat using fun concrete calculations, deduce things about FiniteAdeleRing (𝓞 ℚ) ℚ via the isomorphism) is definitely one approach; I suspect that in some sense we are doing exactly the same thing for the infinite adele ring; the infinite adele ring of Rat is some product over a one-element set of a completion which is not at all defeq to Real, but is uniquely isomorphic to Real.

[Salvatore Mercuri]

Bryan Wang said:

we ideally want statements like the one here relating adicCompletion, which is used in FiniteAdeleRing, to Padic, but apparently this is not in mathlib yet.

This is in mathlib as of last week: #27696 -- should help streamline the Rat proofs!

[Yakov Pechersky]

Yes, and I plan on adding a similar equiv showing Z_p iso to the corresponding Completion (WithVal v_p)

[Yakov Pechersky]

I guess we also need something linking the Completion (WithVal v_p) to adicCompletion pAsIdeal