The proof
We prove the theorem via a series of lemmas.
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.existsE#
There's a compact subset \(E\) of \(D_{\mathbb{A}}\) with the property that for all \(x\in D_{\mathbb{A}}^{(1)}\), the obvious map \(xE\to D\backslash D_{\mathbb{A}}\) is not injective.
Proof
We know that if we pick a \(\mathbb{Q}\)-basis for \(D\) of size \(d\) then this identifies \(D\) with \(\mathbb{Q}^d\), \(D_{\mathbb{A}}\) with \(\mathbb{A}_{\mathbb{Q}}^d\), and \(D\backslash D_{\mathbb{A}}\) with \((\mathbb{Q}\backslash\mathbb{A}_{\mathbb{Q}})^d\). Now \(\mathbb{Q}\) is discrete in \(\mathbb{A}_{\mathbb{Q}}\) by theorem NumberField.AdeleRing.discrete, and the quotient \(\mathbb{Q}\backslash \mathbb{A}_{\mathbb{Q}}\) is compact by theorem Rat.AdeleRing.cocompact. Hence \(D\) is discrete in \(D_{\mathbb{A}}\) and the quotient \(D\backslash D_{\mathbb{A}}\) is compact.
Fix a Haar measure \(\mu\) on \(D_{\mathbb{A}}\) and push it forward to \(D\backslash D_{\mathbb{A}}\); by compactness this quotient has finite and positive measure, say \(m\in\mathbb{R}_{>0}\). Choose any compact \(E\subseteq D_{\mathbb{A}}\) with measure \(> m\) (for example, choose a \(\mathbb{Z}\)-lattice \(L\cong\mathbb{Z}^d\) in \(D\cong\mathbb{Q}^d\), define \(E_f:=\prod_p L_p\in D\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}^\infty\), and define \(E_{\infty}\subseteq D\otimes_{\mathbb{Q}}\mathbb{R}\cong\mathbb{R}^n\) to be a huge closed ball, large enough to ensure the measure of \(E:=E_f\times E_{\infty}\) is bigger than \(m\)). Then \(\mu(xE)=\mu(E)>m\) so the map can't be injective.
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.existsE.
Sources
Used by 1
DefinitionNumberField.AdeleRing.DivisionAlgebra.Aux.E#
We let \(E\) denote any compact set satisfying the hypothesis of the previous lemma.
Uses 1 · Used by 4
DefinitionNumberField.AdeleRing.DivisionAlgebra.Aux.X#
Define \(X:=E-E:=\{e-f:e,f\in E\}\subseteq D_{\mathbb{A}}\).
Uses 1 · Used by 5
DefinitionNumberField.AdeleRing.DivisionAlgebra.Aux.Y#
Define \(Y:=X.X:=\{xy:x,y\in X\}\subseteq D_{\mathbb{A}}\).
Uses 1 · Used by 2
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.X_compact#
\(X\) is a compact subset of \(D_{\mathbb{A}}\).
Proof
It's the continuous image of the compact set \(E\times E\).
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact.
Sources
Uses 1 · Used by 1
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact#
\(Y\) is a compact subset of \(D_{\mathbb{A}}\).
Proof
It's the continuous image of the compact set \(X\times X\).
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact.
Sources
Uses 1 · Used by 1
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel#
If \(\beta\in D_{\mathbb{A}}^{(1)}\) then \(\beta X\cap D^\times\not=\emptyset\).
Proof
Indeed by lemma NumberField.AdeleRing.DivisionAlgebra.Aux.existsE, the map \(\beta E\to D\backslash D_{\mathbb{A}}\) isn't injective, so there are distinct \(\beta e_1,\beta e_2\in \beta E\) with \(e_i\in E\) and \(\beta e_1-\beta e_2=b\in D\). Now \(b\not=0\) and \(D\) is a division algebra, so \(b\in D^\times\). And \(e_1-e_2\in X\) so \(b=\beta(e_1-e_2)\in \beta X\), so we're done.
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel.
Sources
Uses 2 · Used by 1
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'#
Similarly, if \(\beta\in D_{\mathbb{A}}^{(1)}\) then \(X\beta^{-1}\cap D^\times\not=\emptyset\).
Proof
Indeed, \(\beta^{-1}\in D_{\mathbb{A}}^{(1)}\), and so left multiplication by \(\beta^{-1}\) doesn't change Haar measure on \(D_{\mathbb{A}}\), so neither does right multiplication (by theorem addHaarScalarFactor.left_mul_eq_right_mul). So the same argument works: \(E\beta^{-1}\to D\backslash D_{\mathbb{A}}\) is not injective so choose \(e_1\beta^{-1}\not=e_2\beta^{-1}\) with difference \(b\in D\) and then \((e_1-e_2)\beta^{-1}\in D-{0}=D^\times\).
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel'.
Sources
Uses 2 · Used by 1
DefinitionNumberField.AdeleRing.DivisionAlgebra.Aux.T#
Let \(T:=Y\cap D^\times\).
Uses 1 · Used by 2
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.T_finite#
\(T\) is finite.
Proof
It suffices to prove that \(Y\cap D\) is finite. But \(D\subseteq D_{\mathbb{A}}\) is a discrete additive subgroup, and hence closed. And \(Y\subseteq D_{\mathbb{A}}\) is compact. So \(D\cap Y\) is compact and discrete, so finite.
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite.
Sources
Uses 2 · Used by 1
DefinitionNumberField.AdeleRing.DivisionAlgebra.Aux.C#
Define \(C:= (T^{-1}.X) \times X\subset D_{\mathbb{A}}\times D_{\mathbb{A}}\).
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.C_compact#
\(C\) is compact.
Proof
\(X\) is compact and \(T\) is finite.
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact.
Sources
LemmaNumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C#
For every \(\beta\in D_{\mathbb{A}}^{(1)}\), there exists \(b\in D^\times\) and \(\nu\in D_{\mathbb{A}}^{(1)}\) such that \(\beta=b\nu\) and \((\nu,\nu^{-1})\in C.\)
Proof
By lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel, \(\beta X\cap D^\times\not=\emptyset\), and lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel', \(X\beta^{-1}\cap D^\times\not=\emptyset\), so we can write \(\beta x_1=b_1\) and \(x_2\beta^{-1}=b_2\) with \(b_i\in D^\times\) and \(x_i\in X\). Note that \(\beta\in D_{\mathbb{A}}^{(1)}\) and \(b_i\in D^{\times}\subseteq D_{\mathbb{A}}^{(1)}\) by corollary NumberField.AdeleRing.units_mem_ringHaarCharacter_ker, so \(x_i\in D_{\mathbb{A}}^{(1)}\) as well. In particular \(x_i\in D_{\mathbb{A}}^\times\) so \(x_1^{-1}\) makes sense.
Multiplying the equations defining the \(x_i\) and \(b_i\) we deduce that \(x_2x_1=b_2b_1\in Y\cap D^\times=T\) (recall that \(Y=X.X\) and \(T=Y\cap D^\times\) is finite); call this element \(t\). Then \(x_1^{-1}=t^{-1}x_2\in T^{-1}.X\), and \(x_1\in X\), so if we set \(\nu=x_1^{-1}\in D_{\mathbb{A}}^{(1)}\) and \(b=b_1\in D^\times\) then we have \(\beta=b\nu\) and \((\nu,\nu^{-1})\in C := (T^{-1}.X)\times X\). We are done!
Lean
Formalized as NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C.
Sources
Uses 4 · Used by 1
We can now prove Fujisaki's theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient.
The proof of Theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient is shown with its statement.
We note here some useful consequences.
TheoremNumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact#
\(D^\times\backslash(D\otimes_K\mathbb{A}_K^\infty)^\times\) is compact.
Proof
There's a natural map \(\alpha\) from \(D^\times\backslash D_{\mathbb{A}}^{(1)}\) to \(D^\times\backslash (D\otimes_K \mathbb{A}_K^\infty)^\times\). We claim that it's surjective. Granted this claim, we are home, because if we put the quotient topology on \(D^\times\backslash (D\otimes_K \mathbb{A}_K^\infty)^\times\) coming from \((D\otimes_K \mathbb{A}_K^\infty)^\times\) then it's readily verified that \(\alpha\) is continuous, and the continuous image of a compact space is compact.
As for surjectivity: say \(x\in (D\otimes_K \mathbb{A}_K^\infty)^\times\). We need to extend \(x\) to an element \((x,y)\in (D\otimes_K \mathbb{A}_K^\infty)^\times\times(D\otimes_K K_\infty)^\times\) which is in the kernel of \(\delta_{D_{\mathbb{A}}}\). Because \(\delta_{D_{\mathbb{A}}}(x,1)\) is some positive real number, it will suffice to show that if \(r\) is any positive real number then we can find \(y\in (D\otimes_K \mathbb{A}_K^\infty)^\times=(D\otimes_{\mathbb{Q}}\mathbb{R})^\times\) with \(\delta_{D_{\mathbb{A}}}(1,y)=r\), or equivalently (setting \(D_{\mathbb{R}}=D\otimes_{\mathbb{Q}}\mathbb{R}\)) that \(\delta_{D_{\mathbb{R}}}(y)=r\). But \(D\not=0\) as it is a division algebra,and hence \(\mathbb{Q}\subseteq D\), meaning \(\mathbb{R}\subseteq D_{\mathbb{R}}\), and if \(x\in\mathbb{R}^\times\subseteq D_{\mathbb{R}}^\times\) then \(\delta(x)=|x|^d\) with \(d=\dim_{\mathbb{Q}}(D)\), as multiplication by \(x\) is just scaling by a factor of \(x\) on \(D_{\mathbb{R}}\cong\mathbb{R}^d\). In particular we can set \(x=y^{1/d}\).
Lean
Formalized as NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.
Sources
Uses 1 · Used by 1
Remark. In this generality the quotient might not be Hausdorff.
TheoremNumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset#
If \(U\) is an open subgroup of \((D\otimes_K \mathbb{A}_K^\infty)^\times\) then the double coset space \(D^\times\backslash(D\otimes_K \mathbb{A}_K^\infty)^\times/U\) is finite.
Proof
The double cosets give a disjoint open cover of \((D\otimes_K \mathbb{A}_K^\infty)\) which descends to a disjoint open cover of the quotient space \(D^\times\backslash(D\otimes_K \mathbb{A}_K^\infty)^\times\). However this space is compact by theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact.
Lean
Formalized as NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.