Local compactness

As mentioned above, Salvatore Mercuri was the first to give a complete formalisation of the proof that the adele ring is locally compact as a topological space. His work is in his own repo and proved the result using the “ad hoc” topology on the adeles which we initially had. Since then, adeles have been refactored to have the direct limit topology and mathlib has RestrictedProduct.locallyCompactSpace_of_addGroup, the result that a restricted product of topological additive groups \(K_v\) over compact open subgroups \(A_v\) is locally compact.

What we need then is this (note that this is not true for a general Dedekind domain):

TheoremNumberField.instCompactSpaceAdicCompletionIntegers #

If \(K\) is a number field and \(v\) is a nonzero prime ideal of the integers of \(K\), then the integers of \(K_v\) is a compact open subgroup.

Proof

Openness should follow from the fact that the integers are \(\{x : v(x)\lt v(1/\pi)\}\) where \(\pi\) is a uniformizer. Compactness needs finiteness of the residue field \(\mathcal{O}_K/v\).

Lean

Stated as NumberField.instCompactSpaceAdicCompletionIntegers; the blueprint marks no proof of it as formalized.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/AdeleMiniproject.tex, line 74

LeanNumberField.instCompactSpaceAdicCompletionIntegers

Discussionhttps://github.com/ImperialCollegeLondon/FLT/issues/451

Used by 2

Used byNumberField.AdeleRing.locallyCompactSpace · M2.localFullLevel.isCompact

Once we have this, the above result from mathlib gives us

TheoremNumberField.AdeleRing.locallyCompactSpace #

The adeles of a number field are locally compact.

Proof

The adeles of a number field are a product of the finite adeles and the infinite adeles so it suffices to prove that the finite and infinite adeles are locally compact. The infinite adeles are just isomorphic to \(\mathbb{R}^n\) as a topological space, so they're certainly locally compact. As for the finite adeles, the mathlib theorem RestrictedProduct.locallyCompactSpace_of_addGroup says that a restricted product of locally compact additive groups with respect to open compact subgroups is locally compact, so this reduces us the previous result.