A_Q / Q is compact

[kbuzzard]

Suggested proof: show that the canonical map prod_p Z_p x [0,1] -> A_Q -> A_Q / Q is continuous and surjective, and that the source is compact (it being a product of compact spaces). More details on the surjectivity are in the blueprint.

This sorry is in NumberField/AdeleRing.lean.

[4hma4d]

claim

[smmercuri]

I have an almost-complete proof of this here. Note that the proof that Z_p is compact is elsewhere in that repo, and not yet in mathlib as it has some dependencies on another project.

[4hma4d]

I have an almost-complete proof of this here. Note that the proof that Z_p is compact is elsewhere in that repo, and not yet in mathlib as it has some dependencies on another project.

Thanks! I'm working on filling in the sorries. Isn't Z_p compact just PadicInt.compactSpace in Mathlib?

[smmercuri]

So that's compactness for the type PadicInt, whereas the rational adele ring uses HeightOneSpectrum.adicCompletionIntegers ℚ. These two have been shown elsewhere to be equivalent as rings, but it's not in mathlib yet and we would need it to be a topological equivalence in order to use PadicInt.compactSpace.

I should start PR-ing the rest of my repo to mathlib soon, so maybe for now add the following sorried instance before the proof.

instance : CompactSpace (FiniteIntegralAdeles (𝓞 ℚ) ℚ) := sorry