Enter the adeles

The adeles of a number field are discussed in far more detail in the adele miniproject Miniproject: Adeles. We just recall here that if \(K\) is a number field then there are two huge commutative topological \(K\)-algebras called the finite adeles \(\mathbb{A}_K^\infty\) and the adeles \(\mathbb{A}_K\) of \(K\), and that they're both locally compact as topological spaces. We also know from theorem NumberField.AdeleRing.baseChangeEquiv that \(\mathbb{A}_K\cong K\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}K\) (both topologically and algebraically), meaning that if \(R\) is a \(K\)-algebra then \(R_{\mathbb{A}} := R\otimes_K\mathbb{A}_K\) is naturally isomorphic to \(R\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\). One can furthermore check that if \(R\) is a finite \(K\)-algebra then the \(\mathbb{A}_K\)-module topologies and \(\mathbb{A}_{\mathbb{Q}}\)-module topologies on \(R_{\mathbb{A}}\) coincide. Indeed, the topology on \(\mathbb{A}_K\) is the \(\mathbb{A}_{\mathbb{Q}}\)-module topology, as \(\mathbb{A}_K=\mathbb{A}_{\mathbb{Q}}\otimes_{\mathbb{Q}}K\) as topological \(\mathbb{A}_{\mathbb{Q}}\)-algebras, where the right hand side has the \(\mathbb{A}_{\mathbb{Q}}\)-module topology by definition. So the claim follows from the fact that if \(A\) is a topological ring, \(B\) is a topological \(A\)-algebra finite as an \(A\)-module and with the \(A\)-module topology, and if \(M\) is a topological \(B\)-module (and hence a topological \(A\)-module), then the \(A\)-module and \(B\)-module topologies on \(M\) coincide (this is moduleTopology.trans in the repo, not yet PRed to mathlib).

Let \(K\) be a number field and let \(D/K\) be a finite-dimensional central simple \(K\)-algebra (later on \(D\) will be a division algebra (hence the name) but we do not need this yet). Then \(D_{\mathbb{A}}:=D\otimes_K\mathbb{A}_K\) is an \(\mathbb{A}_K\)-algebra which is free of finite rank, and if we give \(D_{\mathbb{A}}\) the \(\mathbb{A}_K\)-module topology then it is a topological ring (by results in mathlib). Furthermore \(D_{\mathbb{A}}\) is free of finite rank over the locally compact topological ring \(\mathbb{A}_K\) and is thus also locally compact. So by the theory of Haar characters (see Chapter Miniproject: Haar Characters) there is a canonical character \(\delta_{D_{\mathbb{A}}}:D_{\mathbb{A}}^\times\to\mathbb{R}_{>0}\) measuring how left multiplication by an element of \(D_{\mathbb{A}}^\times\) changes the additive Haar measure on \(D_{\mathbb{A}}\). Let \(D_{\mathbb{A}}^{(1)}\) denote the kernel of \(\delta_{D_{\mathbb{A}}}\), and give it the subspace topology coming from \(D_{\mathbb{A}}^\times\). Corollary NumberField.AdeleRing.units_mem_ringHaarCharacter_ker from the Haar character miniproject shows that \(D^\times\) (regarded as a subgroup of \(D_{\mathbb{A}}^\times\) via the map \(d\mapsto d\otimes 1\)) is contained within \(D_{\mathbb{A}}^{(1)}\), thus the below theorem typechecks.

TheoremNumberField.AdeleRing.DivisionAlgebra.compact_quotient#

If \(D\) is a division algebra then the quotient \(D^\times\backslash D_{\mathbb{A}}^{(1)}\) with its quotient topology coming from \(D_{\mathbb{A}}^{(1)}\), is compact.

Proof

Indeed, if \(M\) is the preimage of \(C\) under the inclusion \(D_{\mathbb{A}}^{(1)} \to D_{\mathbb{A}}\times D_{\mathbb{A}}\) sending \(\nu\) to \((\nu,\nu^{-1})\), then \(M\) is a closed subspace of a compact space so it's compact (note that \(\delta_{D_{\mathbb{A}}}\) is continuous, by theorem MeasureTheory.ringHaarChar_continuous, so \(D_{\mathbb{A}}^{(1)}\) is a closed subset of \(D_{\mathbb{A}}^\times\) which is itself a closed subset of \(D_{\mathbb{A}}\times D_{\mathbb{A}}\)). Lemma NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C shows that \(M\) surjects onto \(D^\times\backslash D_{\mathbb{A}}^{(1)}\) which is thus also compact.

Lean

Formalized as NumberField.AdeleRing.DivisionAlgebra.compact_quotient.

Sources
Uses 3 · Used by 1

The rest of this miniproject is devoted to a proof of this theorem.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.