Adeles
We finish this miniproject by proving some results about Haar characters for algebras over adele rings. So let \(K\) be a number field and let \(\mathbb{A}_K\) be the adeles of \(K\). We will prove some theorems about \(\mathbb{A}_K\)-algebras \(R\) which are finite and free as \(\mathbb{A}_K\)-modules. Such algebras can be given the \(\mathbb{A}_K\)-module topology and this makes them into locally compact topological rings. In fact we shall only be concerned in applications with algebras of the form \(B\otimes_K\mathbb{A}_K\) where \(B\) is a finite-dimensional \(K\)-algebra. So fix such a \(B\), and write \(B_{\mathbb{A}}\) for \(B\otimes_K\mathbb{A}_K\). Let us first deal with a subtlety. Recall that if \(K\subseteq L\) are number fields, then \(\mathbb{A}_L\) is a module-finite \(\mathbb{A}_K\)-algebra and hence an \(\mathbb{A}_K\)-module, and theorem NumberField.AdeleRing.baseChange_moduleTopology tells us that \(\mathbb{A}_L\) has the \(\mathbb{A}_K\)-module topology. Thus the next lemma applies.
LemmaIsModuleTopology.continuous_bilinear_of_finite_left#
Say \(R\) and \(S\) are topological rings, and \(S\) is an \(R\)-algebra, finite as an \(R\)-module. Assume that the topology on \(S\) is the \(R\)-module topology. Now say \(M\) is an \(S\)-module, and give it the induced \(R\)-module structure. Then the \(R\)-module topology and \(S\)-module topology on \(M\) coincide.
Proof
Let \(i:R\to S\) denote the structure map. First observe that \(S\) has the \(R\)-module topology so the \(R\)-action map \(R\times S\to S\) (explicitly defined by \((r,s)\mapsto i(r)s\)) is continuous, and restricting to \(s=1\) we deduce that \(i\) is continuous.
Now let \(M_R\) and \(M_S\) denote \(M\) with the \(R\)-module and \(S\)-module topologies respectively. It suffices to prove that the identity maps \(M_R\to M_S\) and \(M_S\to M_R\) are continuous. Equivalently, because the \(A\)-module topology on an \(A\)-module is the finest topology making it into a topological module, we need to prove that \(M_R\) is a topological \(S\)-module and that \(M_S\) is a topological \(R\)-module. We start with the latter claim.
First observe that \(M_S\) is a topological \(S\)-module, so addition is continuous. Next note that the map \(R\times M_S\to M_S\) factors through \(S\times M_S\) and is hence the composite of two continuous maps and thus continuous. Hence \(M_S\) is a topological \(R\)-module.
It thus remains to check that \(M_R\) is a topological \(S\)-module, or equivalently that the map \(S\times M_R\to M_R\) is continuous. But this map is \(R\)-bilinear, and by the result Module.continuous_bilinear_of_finite in mathlib, any \(R\)-bilinear map between modules with the \(R\)-module topology is automatically continuous if one of the source modules is finitely-generated. The result applies because \(S\) is assumed to be a finite \(R\)-module and the proof is complete.
Lean
Formalized as IsModuleTopology.continuous_bilinear_of_finite_left.
Sources
Used by 1
CorollaryNumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv#
If \(K\) is a number field and \(V\) is an \(K\)-module, then the natural isomorphism \(V\otimes_K\mathbb{A}_K=V\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\) induced by the natural isomorphism \(\mathbb{A}_K=K\otimes_K\mathbb{A}_{\mathbb{Q}}\) is a homeomorphism if the left hand side has the \(\mathbb{A}_K\)-module topology and the right hand side has the \(\mathbb{A}_{\mathbb{Q}}\)-module topology.
Proof
Lemma IsModuleTopology.continuous_bilinear_of_finite_left tells us that \(V\otimes_K\mathbb{A}_K\) has the \(\mathbb{A}_{\mathbb{Q}}\)-module topology, and it is easily checked that the isomorphism is \(\mathbb{A}_{\mathbb{Q}}\)-linear and hence automatically continuous.
Note that in the Lean we prove this for a general extension \(L/K\) rather than \(K/\mathbb{Q}\).
Lean
Formalized as NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv.
Sources
Uses 1 · Used by 1
As a consequence, if \(B\) is a \(K\)-algebra then we can think of \(B_{\mathbb{A}}\) as either \(B\otimes_K\mathbb{A}_K\) with the \(\mathbb{A}_K\)-module topology or as \(B\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\) with the \(\mathbb{A}_{\mathbb{Q}}\)-module topology. Note that this isomorphism commutes with the inclusions from \(B\) into these rings. But Lean is picky about these things so we'll have to be careful.
TheoremNumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul#
Let \(B\) be a finite-dimensional central simple \(K\)-algebra. Say \(u\in B_{\mathbb{A}}^\times\), and define \(\ell_u\) and \(r_u:B_{\mathbb{A}}\to B_{\mathbb{A}}\) by \(\ell_u(x)=ux\) and \(r_u(x)=xu\). Then \(d_{B_{\mathbb{A}}}(\ell_u)=d_{B_{\mathbb{A}}}(r_u)\).
Proof
We think of \(B_{\mathbb{A}}\) as \(B\otimes_K\mathbb{A}_K\). If \(u=(u_v)\) as \(v\) runs through the places of \(K\) then \(d_{B_{\mathbb{A}}}(\ell_u)=\prod_v d_{B_v}(\ell_{u_v})\) by theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight (and the product is finite). By corollary IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight this equals \(\prod_v d_{B_v}(r_{u_v})\), and again by theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight this is \(d_{B_{\mathbb{A}}}(r_u)\).
Lean
Stated as NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul; the blueprint marks no proof of it as formalized.
Sources
The previous theorem only applies to inner forms of matrix algebras, but the below theorem, a generalization of the adelic product formula, is valid for any finite-dimensional \(K\)-algebra. Before we state it let's remind ourselves of the product formula for \(\mathbb{Q}\), and restate it in the language of these Haar characters.
LemmaMeasureTheory.ringHaarChar_adeles_rat#
If \(x\in\mathbb{A}_{\mathbb{Q}}^\times\) then \(\delta_{\mathbb{A}_{\mathbb{Q}}}(x)=\prod_v|x_v|_v.\)
Proof
By theorem MeasureTheory.addEquivAddHaarChar_prodCongr we have \(\delta_{\mathbb{A}_{\mathbb{Q}}}(x)=\delta_{\mathbb{A}_{\mathbb{Q}}^\infty}(x^\infty)\times\delta_{\mathbb{R}}(x_\infty)\). By lemma MeasureTheory.ringHaarChar_real we have \(\delta_{\mathbb{R}}(x_\infty)=|x|_\infty\), and by theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight we have \(\delta_{\mathbb{A}_{\mathbb{Q}}^\infty}=\prod_p\delta_{\mathbb{Q}_p}(x_p)\). By lemma MeasureTheory.ringHaarChar_padic we have \(\delta_{\mathbb{Q}_p}(x_p)=|x_p|_p\) and putting everything together we get the result.
Lean
Formalized as MeasureTheory.ringHaarChar_adeles_rat.
Sources
Now \(\mathbb{A}_{\mathbb{Q}}\) is nonzero a \(\mathbb{Q}\)-algebra and hence we have an inclusion \(\mathbb{Q}^\times\to\mathbb{A}_{\mathbb{Q}}^\times\). Here is our reinterpretation of the product formula.
LemmaMeasureTheory.ringHaarChar_adeles_units_rat_eq_one#
If \(x\in\mathbb{Q}^\times\subseteq\mathbb{A}_{\mathbb{Q}}^\times\) then \(\delta_{\mathbb{A}_{\mathbb{Q}}}(x)=1.\)
Proof
By lemma MeasureTheory.ringHaarChar_adeles_rat we have \(\delta_{\mathbb{A}_{\mathbb{Q}}}(x)=\prod_v|x|_v\). But the product formula says that this is 1. A quick proof: if \(x=\pm\prod_pp^{e_p}\) then \(\prod_p|x|_p=\prod_pp^{-e_p}\) and \(|x|_\infty=\prod_pp^{e_p}\) so they cancel.
Lean
Formalized as MeasureTheory.ringHaarChar_adeles_units_rat_eq_one.
Sources
Uses 1
Next we generalize this to finite-dimensional \(\mathbb{Q}\)-vector spaces.
So say \(V\) is an \(N\)-dimensional \(\mathbb{Q}\)-vector space, and define \(V_{\mathbb{A}}:= V\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\) with its \(\mathbb{A}_{\mathbb{Q}}\)-module topology. If we choose an isomorphism \(V\cong\mathbb{Q}^N\) then \(V_{\mathbb{A}}\cong\mathbb{A}_{\mathbb{Q}}^N\) as an additive topological abelian group. In particular, \(V_{\mathbb{A}}\) is locally compact.
Fix a \(\mathbb{Q}\)-linear automorphism \(\phi:V\to V\). By base extension \(\phi\) induces an \(\mathbb{A}_{\mathbb{Q}}\)-linear automorphism \(\phi_{\mathbb{A}}\) of \(V_{\mathbb{A}}\) which is also a homeomorphism of \(V_{\mathbb{A}}\) if \(V_{\mathbb{A}}\) is given the module topology as an \(\mathbb{A}_{\mathbb{Q}}\)-module. Our goal is
TheoremMeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one#
In the above situation (\(V\) a finite-dimensional \(\mathbb{Q}\)-vector space, \(\phi:V\cong V\) is \(\mathbb{Q}\)-linear, \(\phi_{\mathbb{A}}\) the base extension to \(V_{\mathbb{A}}:=V\otimes_{\mathbb{Q}}{\mathbb{A}_{\mathbb{Q}}}\), a continuous linear endomorphism of \(V_{\mathbb{A}}\) with the \(\mathbb{A}_{\mathbb{Q}}\)-module topology), we have \(d_{V_{\mathbb{A}}}(\phi_{\mathbb{A}})=1.\)
Proof
The original blueprint proof of this was that \(\phi_{\mathbb{A}} : V_{\mathbb{A}}\to V_{\mathbb{A}}\) could be written as a restricted product of \(\phi_v:V\otimes_{\mathbb{Q}}{\mathbb{Q}_v} \to V\otimes_{\mathbb{Q}}\mathbb{Q}_v\) and hence by theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight we have \(d_{V_{\mathbb{A}}}(\phi_{\mathbb{A}})=\prod_p d_{V_p}(\phi_p)\times d_{V_\infty}(\phi_\infty)\), and then applying Lemma MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det this is equal to \(\prod_v\delta_{\mathbb{Q}_v}(\det(\phi_v))\prod_v\delta_{\mathbb{Q}_v}(\det(\phi))=1\).
This turned out to be a nightmare to formalize, because commuting the tensor product and the restricted product cannot be done naively, as the tensor product is over \(\mathbb{Q}\) and the submodules in the restricted product defining \(\mathbb{A}_{\mathbb{Q}}\) are not \(\mathbb{Q}\)-modules. So one has to choose a \(\mathbb{Z}\)-lattice in \(V\) and use the isomorphisms \(V\otimes_{\mathbb{Q}}\mathbb{A}=\Lambda\otimes_{\mathbb{Z}}\mathbb{A}= \Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_\infty\times\prod'_p[\Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_p;\Lambda\otimes_{\mathbb{Z}}\mathbb{Z}_p]= V\otimes_{\mathbb{Q}}\mathbb{Q}_\infty\times\prod'_p[V\otimes_{\mathbb{Q}}\mathbb{Q}_p;im(\Lambda\otimes_{\mathbb{Z}}\mathbb{Z}_p)]\) and check that all of these canonical maps are continuous (and one of these claims boils down to yet another claim of the form "if you do something to the factors and then take the restricted product, then this is topologically the same as doing it to the restriced product", with the thing being \(\Lambda\otimes_{\mathbb{Z}}\) in this case, something which needs checking).
So here is the proof which we actually formalized. Say an automorphism of a finite free \(R\)-module is nice if it's a product of transvections and diagonal matrices with unit entries. Mathlib has the fact that if \(R\) is a field then all automorphisms are nice, and the base change of a nice morphism is nice. Hence \(\phi_{\mathbb{A}}\) is nice, and we can simply prove Lemma (MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det) for nice endomorphisms over a commutative ring, which gives the result we want immediately by the product formula.
Lean
Formalized as MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one.
Sources
CorollaryNumberField.AdeleRing.units_mem_ringHaarCharacter_ker#
If \(B\) is a finite-dimensional \(\mathbb{Q}\)-algebra (for example a number field, or a quaternion algebra over a number field), if \(B_{\mathbb{A}}\) denotes the ring \(B\otimes_{\mathbb{Q}}\mathbb{A}_{\mathbb{Q}}\), and if \(b\in B^\times\), then \(\delta_{B_{\mathbb{A}}}(b)=1\).
Proof
Follows immediately from the previous theorem.
Lean
Formalized as NumberField.AdeleRing.units_mem_ringHaarCharacter_ker.
Sources
Uses 1
CorollaryNumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one#
If \(B\) is a finite-dimensional \(\mathbb{Q}\)-algebra and if \(b\in B^\times\) then right multiplication by \(b\) does not change Haar measure on \(B_{\mathbb{A}}\).
Proof
Follows immediately from the previous theorem.
Lean
Formalized as NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.