If \(\mu '\) is a second choice then \(\mu '=\lambda \mu \) for some positive real \(\lambda \), and the \(\lambda \)s on each side of \(\mu '(X)=d_A(\phi )(\phi _*\mu ')(X)\) cancel.

This is a restatement of the previous result.

This follows from lemma 9.3 applied to the regular Haar measure \(\phi ^*\mu \) and the fact that \(\phi _*\phi ^*\mu =\mu \).

This follows immediately from lemma 9.3 and the definition of the pushforward of a measure.

This also follows immediately from lemma 9.3.

This is immediate from corollary 9.4.

Clear.

Here’s one way: it suffices to prove that \(d_A(\phi \circ \psi )(\phi \circ \psi )_*\mu =d_A(\phi )d_A(\psi )(\phi \circ \psi )_*\mu \) (because there exists a compact set with positive finite measure) and using lemma 9.3 and the fact that \((\phi \circ \psi )_*\mu =\phi _*(\psi _*\mu )\) one can simplify both sides to \(\mu \).

A short calculation using lemma 9.6.

Immediate from lemma 9.5.

Fix a Haar measure \(\mu \) on \(R\) and a continuous real-valued function \(f\) on \(R\) with compact support and such that \(\int f(x) d\mu (x)\not=0\). Then \(r \mapsto \int f(rx) d\mu (x)\) is a continuous function from \(R\to \mathbb {R}\) (because a continuous function with compact support is uniformly continuous) and thus gives a continuous function \(R^\times \to \mathbb {R}\). Thus the function \(u\mapsto (\int f(ux) d\mu (x))/(\int f(x)d\mu (x))\) is a continuous function from \(R^\times \) to \(\mathbb {R}\) taking values in \(\mathbb {R}_{{\gt}0}\). Hence \(\delta _R^{-1}\) is continuous, from lemma 9.11, and thus \(\delta _R\) is too.

Take \(\mu \) to be Lebesgue measure and \(X=[0,1]\). We have \(\delta (u)=\mu (uX)\). If \(u{\gt}0\) then \(u[0,1]=[0,u]\) which has measure \(u=|u|\), and if \(u{\lt}0\) then \(u*[0,1]=[u,0]\) which has measure \(-u=|u|\).

Multiplication by a positive real \(r\) sends a unit square to a square of area \(r^2=|r|^2\). Multiplication by \(e^{i\theta }\) is a rotation and thus does not change area. The general case follows.

Normalise Haar measure so that \(\mu (\mathbb {Z}_p)=1\). If \(u\) is a \(p\)-adic unit then \(u\mathbb {Z}_p=\mathbb {Z}_p\) so multiplication by \(u\) didn’t change Haar measure. If however \(u=p\) then \(u\mathbb {Z}_p\) has index \(p\) in \(\mathbb {Z}_p\) and, because \(\mu (i+p\mathbb {Z}_p)=\mu (p\mathbb {Z}_p)\) we have that \(\mu (\mathbb {Z}_p)=p\mu (p\mathbb {Z}_p)\) and thus \(\delta (p)=p^{-1}\). These elements generate \(\mathbb {Q}_p^\times \) and two characters which agree on generators of a group must agree on the group.

The proof should be inspired by Real.map_matrix_volume_pi_eq_smul_volume_pi, which crucially uses the induction principle Matrix.diagonal_transvection_induction_of_det_ne_zero. In short, one needs to check it for diagonal matrices and for matrices which are the identity except that one off-diagonal entry is non-zero, because these matrices generate \(GL_n(F)\) if \(F\) is a field. Note that we only need the result for \(F=\mathbb {R}\) and \(F=\mathbb {Q}_p\) (and possibly for finite extensions of these depending on which route we go for some intermediate results), so if it helps we can assume that \(F\) is second countable (but it shouldn’t be necessary).

Follows immediately from the preceding lemma.

Determinants are unchanged by base extension, so WLOG \(k\) is algebraically closed. Then it’s known that \(B\) must be a matrix algebra, say \(M_n(k)\). Now \(u\) can be thought of as a matrix which has its own intrinsic determinant \(d\), and \(B\) as a left \(B\)-module becomes a direct sum of \(n\) copies of \(V\), the standard \(n\)-dimensional representation of \(B\). Thus \(\det (\ell _u)=d^n\). Similarly \(\det (r_u)=d^n\) and in particular they are equal.

If \(\ell _u\) and \(r_u\) denote left and right multiplication by \(u\) on \(B\), then we have seen in lemma 9.18 that \(d_B(r_u)=\delta _F(\det (r_u))\). Lemma 9.20 tells us that this is \(\delta _F(\det (\ell _u))\) and this is \(\delta _B(u)\) again by corollary 9.18.

We only need this result in the case where both \(A\) and \(B\) are second-countable, in which case Prod.borelSpace can be used to show that Haar measure on \(A\times B\) is the product of Haar measures on \(A\) and \(B\), and in this case the result follows easily. Without this assumption, the product of these measures may not even be a Borel measure and one has to be more careful. The proof in this case is explained by Gouëzel here. Here is the idea. Let \(\rho \) be a Haar measure on \(A\times B\). Fix sets \(X\subseteq A\) and \(Y\subseteq B\) which are compact with nonempty interior. We can now pull back \(\rho \) to a measure \(\nu \) on the Borel sigma-algebra of \(A\) defined as \(\nu (s)=\rho (s\times Y)\) and this is easily checked to be a Haar measure on \(A\). Then \(\delta _{A\times B}(a,0)\nu (X)= \delta _{A\times B}(a,0)\rho (X\times Y)=\rho ((a,0)(X\times Y))= \rho (aX\times Y)=\nu (aX)=\delta _A(a)\nu (X)\) , so \(\delta _{A\times B}(a,0)=\delta _A(a)\). Similarly \(\delta _{A\times B}(0,b)=\delta _B(b)\) and because \(\delta _{A\times B}\) is a group homomorphism we’re home.

Induction on the size of the finite set, using the previous lemma.

Follows immediately from lemma 9.22.

Follows immediately from lemma 9.23.

Translation-invariance is easy, compact sets are finite because continuous image of compact is compact, open sets are bounded because image of open is open.

Again this is because the image of compact is compact and the image of open is open, so all the properties of being a regular measure are easily checked.

We have \(d_A(\phi )\mu (A)=\mu (A)\) from lemma 9.5 and \(\mu (A)\) is positive and finite because \(A\) is open and compact.

Choose a regular Haar measure \(\mu _B\) on \(B\). We just saw in lemmas 9.26 and 9.27 that its pullback \(\mu _A:=f^*\mu _B\) to \(A\) is also a regular Haar measure. Now fix a continuous compactly-supported function \(g\) on \(A\) with \(0{\lt}\int g(a)d\mu (a){\lt}\infty \). Then \(d_A(\alpha )\int g(a)d\mu _A(a)=\int g(a)d(\alpha ^*\mu _A)(a)\) by lemma 9.7. This equals \(\int g(a)d(\alpha ^* f^*\mu _B)(a)\) by definition, which is \(\int g(a)d(f^*\beta ^*\mu _B)(a)\) because pullback of pullback is pullback. This equals \(d_B(\beta )\int g(a) d(f^*\mu _B)(a)\) by corollary 9.4 which is \(d_B(\beta )\int g(a)d\mu _A(a)\) by definition, and so \(d_A(\alpha )=d_B(\beta )\) as required.

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.

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 9.29 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\). 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 9.28. Finally \(\delta (\prod _{i\in S}\phi _i)=\prod _{i\in S}\delta (\phi _i)\) by lemma 9.23 and we are home.

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 9.31 applies.

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.

Lemma 9.33 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}\).

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 9.31 (and the product is finite). By corollary 9.21 this equals \(\prod _v d_{B_v}(r_{u_v})\), and again by theorem 9.31 this is \(d_{B_{\mathbb {A}}}(r_u)\).

By theorem 9.22 we have \(\delta _{\mathbb {A}_{\mathbb {Q}}}(x)=\delta _{\mathbb {A}_{\mathbb {Q}}^\infty }(x^\infty )\times \delta _{\mathbb {R}}(x_\infty )\). By lemma 9.14 we have \(\delta _{\mathbb {R}}(x_\infty )=|x|_\infty \), and by theorem 9.31 we have \(\delta _{\mathbb {A}_{\mathbb {Q}}^\infty }=\prod _p\delta _{\mathbb {Q}_p}(x_p)\). By lemma 9.16 we have \(\delta _{\mathbb {Q}_p}(x_p)=|x_p|_p\) and putting everything together we get the result.

By lemma 9.36 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.

Fix once and for all a \(\mathbb {Z}\)-lattice \(L\subseteq V\) (that is, a spanning \(\mathbb {Z}^N\) in the \(\mathbb {Q}^N\)). Then \(V\otimes _{\mathbb {Q}}\mathbb {A}_{\mathbb {Q}}=L\otimes _{\mathbb {Z}}\mathbb {A}_{\mathbb {Q}}\) which is \(L\otimes _{\mathbb {Z}}(\mathbb {A}_{\mathbb {Q}}^\infty \times \mathbb {R})\). Because tensoring by a finitely presented module commute with restricted products and binary products this equals \(\prod '_p(L\otimes _{\mathbb {Z}}\mathbb {Q}_p)\times (L\otimes _{\mathbb {Q}}\mathbb {R})\), the restricted product being over \(L\otimes _{\mathbb {Z}}\mathbb {Z}_p\), and this is \(\prod '_p(V\otimes _{\mathbb {Q}}\mathbb {Q}_p)\times (V\otimes _{\mathbb {Q}}\mathbb {R})\). If \(V_v\) denotes \(V\otimes _{\mathbb {Q}}\mathbb {Q}_v\) then the endomorphism \(\phi _{\mathbb {A}}\) is the product of \(\phi _p\) for all \(p\) and \(\phi _\infty \), where \(\phi _v\) is a \(\mathbb {Q}_v\)-linear and and hence continuous automorphism of \(V_v\).

Hence by theorem 9.31 we have \(d_{V_{\mathbb {A}}}(\phi _{\mathbb {A}})=\prod _p d_{V_p}(\phi _p)\times d_{V_\infty }(\phi _\infty )\), where we note that all but finitely many of the \(d_{V_p}(\phi _p)\) are 1.

By Lemma 9.18 we have that \(d_{V_v}(\phi _v)=\delta _{\mathbb {Q}_v}(\det (\phi _v))\), hence \(d_{V_{\mathbb {A}}}(\phi _{\mathbb {A}})=\prod _v\delta _{\mathbb {Q}_v}(\det (\phi _v))\). But \(\det (\phi _v)\) is equal to the determinant of \(\phi \) on \(V\) as \(\mathbb {Q}\)-vector space (because base change does not change determinant), which is some nonzero rational number \(q\). Thus \(d_{V_{\mathbb {A}}}(\phi _{\mathbb {A}})=\prod _v\delta _{\mathbb {Q}_v}(q)=1\) by the product formula for \(\mathbb {Q}\).

Follows immediately from the previous theorem.

Follows immediately from the previous theorem.