Restricted products
Now say \(A=\prod'_i A_i\) is the restricted product of a collection of types \(A_i\) with respect to the subsets \(C_i\). Recall that this is the subset of \(\prod_i A_i\) consisting of y Say \(B=\prod'_i B_i\) is the restricted product of types \(B_i\) over the same index set, with respect to subsets \(D_i\). Say \(\phi_i:A_i\to B_i\) are functions with the property that \(\phi_i(C_i)\subseteq D_i\) for all but finitely many \(i\). It is easily checked that the \(\phi_i\) induce a function \(\phi:=\prod'_i\phi_i:A\to B\). It is also easily checked that if all the \(A_i\) and \(B_i\) are groups or rings or \(R\)-modules, the \(C_i\) and \(D_i\) are subgroups or subrings or submodules, and the \(\phi_i\) are group or ring or module homomorphisms, then \(\phi\) is a group or ring or module homomorphism. However topological facts lie a little deeper.
LemmaContinuous.restrictedProduct_congrRight#
If the \(A_i\) and \(B_i\) are topological spaces and the \(\phi_i\) are continuous functions, then the restricted product \(\phi = \prod'_i\phi_i\) is a continuous function.
Proof
We use the universal property RestrictedProduct.continuous_dom of the topology in mathlib to reduce to the claim that for all finite \(S\), the induced map \(A_S:=\prod_{i\in S}A_i\times\prod_{i\notin S}C_i\to B\) is continuous. Because the inclusion \(A_S\to A_T\) is continuous for \(S\subseteq T\) we are reduced to checking this claim for \(S\) sufficiently large that it contains all of the \(i\) for which \(\phi(C_i)\not=D_i\). For such \(S\), this map \(A_S\to B\) factors as \(A_S\to B_S\to B\) and \(B_S\to B\) is continuous, so it suffices to prove that \(A_S\to B_S\) is continuous, but this is just a product of continuous maps.
Lean
Formalized as Continuous.restrictedProduct_congrRight.
Sources
We now focus on the case that \(B_i=A_i\) are locally compact groups, \(D_i=C_i\) are compact open subgroups, and \(\phi_i:A_i\to A_i\) are group isomorphisms and homeomorphisms sending \(C_i\) onto \(C_i\) for all but finitely many \(i\). Then the restricted product \(A:=\prod'A_i\) of the \(A_i\) with respect to the \(C_i\) is also a locally compact topological group, and the restricted product \(\phi=\prod'\phi_i\) of the \(\phi_i\) is a group isomorphism and homeomorphism, so we can ask how \(d_A(\phi)\) compares to the \(d_{A_i}(\phi_i)\).
First note that \(d_{A_i}(\phi_i)=1\) for all the \(i\) such that \(\phi_i(C_i)=C_i\), as \(d_{A_i}(\phi_i)\) can be computed as \(\mu(\phi_i(C_i))/\mu(C_i)\) and \(\mu(C_i)\) is guaranteed to have positive finite measure as it is open and compact. Hence the product \(\prod_id_{A_i}\phi_i\) is a finite product, in the sense that all but finitely many terms are 1. The following theorem shows that the value of this product is \(d(\phi)\).
TheoremMeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight#
With \(A\), \(A_i\), \(C_i\), \(\phi_i\), \(\phi\) defined as above, we have \(\delta_A(\phi)=\prod_i\delta_{A_i}(\phi_i)\).
Lean
Stated as MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight; the blueprint marks no proof of it as formalized.
Sources
Remark. In the Lean file we make the additional assumption that the index set over which we're taking the product, is countable, and that the \(A_i\) are second countable. This is because in this proof we make use of an infinite product \(\prod_{i\notin S}C_i\) of topological spaces equipped with Haar measure, so each topological space gets equipped with the Borel sigma algebra. Mathlib then gives the product a canonical product sigma algebra which, in the case where the index set is uncountable, may not be the Borel sigma algebra. However we also want to use Haar measure on the product so we need the “canonical” sigma algebra on this product to be the Borel sigma algebra. Rather than taking the trouble to locally turn off this product sigma algebra construction in FLT, we simply restrict to a countable index set and add second countability assumptions, because then the product is a Borel sigma algebra and this is all we need in our applications to adeles.
Proof. Assume \(\phi_i(C_i)=C_i\) for all \(i\not\in S\), a finite set, and work in the open subgroup \(U:=\prod_{i\in S}A_i\times\prod_{i\not\in S}C_i\). Then \(\phi\) induces an automorphism \(\phi_S\) of this open subgroup \(U\) of \(A\), and in particular lemma MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding tells us that \(\delta(\phi)=\delta_U(\phi_S)\). Next note that \(\phi_S:U\to U\) can be written as a product of the automorphisms \(\prod_{i\not\in S}\phi_i|_{C_i}\) of \(\prod_{i\not\in S}C_i\) and \(\prod_{i\in S}\phi_i\) of \(\prod_{i\in S}A_i\), so by lemma MeasureTheory.addEquivAddHaarChar_prodCongr we have \(\delta(\phi)=\delta(\prod_{i\not\in S}\phi_i|_{C_i})\times\delta(\prod_{i\in S}\phi_i).\) Because \(\prod_{i\not\in S}C_i\) is a compact group we must have \(\delta(\phi_{i\not\in S}\phi_i|_{C_i})=1\) by lemma MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace. Finally \(\delta(\prod_{i\in S}\phi_i)=\prod_{i\in S}\delta(\phi_i)\) by lemma MeasureTheory.addEquivAddHaarChar_piCongrRight and we are home.
As a special case, if \(R\) is the restricted product of a collection of topological rings \(R_i\) (not necessarily commutative) each equipped with a compact open subring \(C_i\), then we have
CorollaryMeasureTheory.ringHaarChar_restrictedProduct#
If \(u=(u_i)_i\in R^\times\) then \(\delta_R(u)=\prod_i\delta_{R_i}(u_i)\).
Proof
By definition of restricted product we have \(u_i\in C_i\) for all but finitely many \(i\). Note also that \(u\) has an inverse \(v=(v_i)_i\) with \(v_i\in C_i\) for all but finitely many \(i\). The fact that \(u_iv_i=v_iu_i=1\) means that \(u_i,v_i\in C_i^\times\) for all but finitely many \(i\). Thus the previous theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight applies.
Lean
Formalized as MeasureTheory.ringHaarChar_restrictedProduct.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.