8 Miniproject: Adeles
8.1 Status
This is an active miniproject.
8.2 The goal
There are several goals to this miniproject.
Define the adeles \(\mathbb {A}_K\) of a number field \(K\) and give them the structure of a \(K\)-algebra (status: now in mathlib thanks to Salvatore Mercuri);
Prove that \(\mathbb {A}_K\) is a locally compact topological ring (status: also proved by Mercuri but not yet in mathlib);
Base change: show that if \(L/K\) is a finite extension of number fields then the natural map \(L\otimes _K\mathbb {A}_K\to \mathbb {A}_L\) is an isomorphism, both algebraic and topological; (status: not formalized yet, but there is a plan – see the project dashboard);
Prove that \(K \subseteq \mathbb {A}_K\) is a discrete subgroup and the quotient is compact (status: not formalized yet, but there is a plan – see the project dashboard);
Get this stuff into mathlib (status: (1) done, (2)–(4) not done).
We briefly go through the basic definitions. Let \(K\) be a number field. Let \(\widehat{\mathbb {Z}}=\projlim _{N\geq 1}(\mathbb {Z}/N\mathbb {Z})\) be the profinite completion of \(\mathbb {Z}\), equipped with the projective limit topology.
A cheap definition of the finite adeles \(\mathbb {A}_K^\infty \) of \(K\) is \(K\otimes _{\mathbb {Z}}\widehat{\mathbb {Z}}\), equipped with the \(\widehat{\mathbb {Z}}\)-module topology. A cheap definition of the infinite adeles \(K_\infty \) of \(K\) is \(K\otimes _{\mathbb {Q}}\mathbb {R}\) with the \(\mathbb {R}\)-module topology (this is a finite-dimensional \(\mathbb {R}\)-vector space so this is just the usual topology on \(\mathbb {R}^n\)). A cheap definition of the adeles of \(K\) is \(\mathbb {A}_K^\infty \times K_\infty \) with the product topology. This is a commutative topological ring.
However in the literature (and in mathlib) we see different definitions. The finite adeles of \(K\) are usually defined in the books as the so-called restricted product \(\prod '_{\mathfrak {p}}K_{\mathfrak {p}}\) over the completions \(K_{\mathfrak {p}}\) of \(K\) at all maximal ideals \(\mathfrak {p}\subseteq \mathcal{O}_K\) of the integers of \(K\). Here the restricted product is the subset of \(\prod _{\mathfrak {p}}K_{\mathfrak {p}}\) consisting of elements which are in the integers \(\mathcal{O}_{K,\mathfrak {p}}\) of \(K_{\mathfrak {p}}\) for all but finitely many \(\mathfrak {p}\). This is the definition given in mathlib. Mathlib also has the proof that they’re a topological ring; furthermore the construction of the finite adeles in mathlib works for any Dedekind domain (this was pointed out to me by María Inés de Frutos Fernández; the adeles are an arithmetic object, but the finite adeles are an algebraic object).
Similarly the infinite adeles of a number field \(K\) are usually defined as \(\prod _v K_v\), the product running over the archimedean completions of \(K\), and this is the mathlib definition.
The adeles of a number field \(K\) are the product of the finite and infinite adeles, and mathlib knows that they’re a \(K\)-algebra and a topological ring.
8.3 Local compactness
As mentioned above, Salvatore Mercuri was the first to give a complete formalisation of the proof that the adele ring is locally compact as a topological space. His work is in his own repo and proved the result using the “ad hoc” topology on the adeles which we initially had. Since then, adeles have been refactored to have the direct limit topology and mathlib has RestrictedProduct.locallyCompactSpace_of_addGroup, the result that a restricted product of topological additive groups \(K_v\) over compact open subgroups \(A_v\) is locally compact.
What we need then is this (note that this is not true for a general Dedekind domain):
If \(K\) is a number field and \(v\) is a nonzero prime ideal of the integers of \(K\), then the integers of \(K_v\) is a compact open subgroup.
Openness should follow from the fact that the integers are \(\{ x : v(x){\lt}v(1/\pi )\} \) where \(\pi \) is a uniformizer. Compactness needs finiteness of the residue field \(\mathcal{O}_K/v\).
Once we have this, the above result from mathlib gives us
The adeles of a number field are locally compact.
The adeles of a number field are a product of the finite adeles and the infinite adeles so it suffices to prove that the finite and infinite adeles are locally compact. The infinite adeles are just isomorphic to \(\mathbb {R}^n\) as a topological space, so they’re certainly locally compact. As for the finite adeles, the mathlib theorem RestrictedProduct.locallyCompactSpace_of_addGroup says that a restricted product of locally compact additive groups with respect to open compact subgroups is locally compact, so this reduces us the previous result.
8.4 Base change
The “theorem” we want is that if \(L/K\) is a finite extension of number fields, then \(\mathbb {A}_L=L\otimes _K\mathbb {A}_K\). This isn’t a theorem though, this is actually a definition (the map between the two objects) and a theorem about the definition (that it’s an isomorphism). In fact the full claim is that it is both a homeomorphism and an \(L\)-algebra isomorphism. Before we can prove the theorem, we need to make the definition.
Recall that the adeles \(\mathbb {A}_K\) of a number field is a product \(\mathbb {A}_K^\infty \times K_\infty \) of the finite adeles and the infinite adeles. So our “theorem” follows immediately from the “theorem”s that \(\mathbb {A}_L^\infty =L\otimes _K\mathbb {A}_K^\infty \) and \(L_\infty =L\otimes _KK_\infty \) (both of these equalities mean an algebraic and topological isomorphism). We may thus treat the finite and infinite results separately.
8.4.1 Base change for nonarchimedean completions.
As pointed out above, the theory of finite adeles works fine for Dedekind domains. So for the time being let \(A\) be a Dedekind domain. Recall that the height one spectrum of \(A\) is the nonzero prime ideals of \(A\). Note that because we stick to the literature, rather than to common sense, fields are Dedekind domains in mathlib, and the height one spectrum of a field is empty. The reason I don’t like allowing fields to be Dedekind domains is that geometrically the definition of Dedekind domain in the literature is “smooth affine curve, or a point”. But many theorems in algebraic geometry begin “let \(C\) be a smooth curve”, rather than “let \(C\) be a smooth curve or a point”.
Let \(K\) be the field of fractions of \(A\). If \(v\) is in the height one spectrum of \(A\), then we can put the \(v\)-adic topology on \(A\) and on \(K\), and consider the completions \(A_v\) and \(K_v\). The finite adele ring \(\mathbb {A}_{A,K}^\infty \) is defined to be the restricted product of the \(K_v\) with respect to the \(A_v\), as \(v\) runs over the height one spectrum of \(A\). It is topologised by making \(\prod _v A_v\) open with the product topology (here \(A_v\) has the \(v\)-adic topology).
Now let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\). We want to relate the finite adeles of \(K\) and of \(L\). We work place by place, starting by fixing one place \(w\) of \(B\) and analysing the relation of \(L_w\) and \(B_w\) to the completions \(K_v\) and \(A_v\) where \(v\) is the place of \(A\) dividing \(w\).
So let \(w\) be a nonzero prime ideal of \(B\). Say \(w\) lies over \(v\), a prime ideal of \(A\). Then we can put the \(w\)-adic topology on \(L\) and the \(v\)-adic topology on \(K\). Furthermore we can equip \(K\) with an additive \(v\)-adic valuation, that is, a function also called \(v\) from \(K\) to \(\mathbb {Z}\cup \{ \infty \} \) normalised so that if \(\pi \) is a uniformiser for \(v\) then \(v(\pi )=1\). Similarly we consider \(w\) as a function from \(L\) to \(\mathbb {Z}\cup \{ \infty \} \). The next lemma explains how these valuations are related.
If \(i:K\to L\) denotes the inclusion then for \(k\in K\) we have \(e\times w(i(k))=v(k)\), where \(e\) is the ramification index of \(w/v\) (recall that valuations here are written additively, unlike in mathlib).
Standard (and formalized).
There’s a natural ring map \(K_v\to L_w\) extending the map \(K\to L\). It is defined by completing the inclusion \(K\to L\) at the finite places \(v\) and \(w\) (which can be done because the previous lemma shows that the map is uniformly continuous for the \(v\)-adic and \(w\)-adic topologies).
If \(i_v:K_v\to L_w\) denotes the map of the previous definition then for \(x\in K_v\) we have \(e\times w(i(k))=v(k)\), where \(e\) is the ramification index of \(w/v\).
Follows by continuity from lemma 8.3.
The map \(i_v:K_v\to L_w\) sends the integer ring \(A_v\) into \(B_w\).
The integer ring is defined by \(v\geq 0\) (or \(v\leq 1\) in mathlib, which uses multiplicative valuations) so the result follows from 8.5.
Giving \(L_w\) the \(K_v\)-algebra structure coming from the natural map \(K_v\to L_w\), the \(w\)-adic topology on \(L_w\) is the \(K_v\)-module topology.
Any basis for \(L\) as a \(K\)-vector space spans \(L_w\) as a \(K_v\)-module, so \(L_w\) is finite-dimensional over \(K_v\) and the module topology is the same as the product topology. So we need to establish that the product topology on \(L_w=K_v^n\) is the \(w\)-adic topology. But the \(w\)-adic topology is induced by the \(w\)-adic norm, which makes \(L_w\) into a normed \(K_v\)-vector space, and (after picking a basis) the product norm on \(L_w=K_v^n\) also makes \(L_w\) into a normed \(K_v\)-vector space. So the result follows from the standard fact (see for example the lemma on p52 of Cassels-Froelich, formalized as ContinuousLinearEquiv.ofFinrankEq in mathlib) that any two norms on a finite-dimensional vector space over a complete field are equivalent (and thus induce the same topology).
Because of the commutative diagram
we can view \(L_w\) as an \(L\otimes _KK_v\)-algebra.
Now instead of fixing \(w\) upstairs, we fix \(v\) downstairs and consider all \(w\) lying over it at once. So say \(v\) is in the height one spectrum of \(A\).
There are only finitely many primes \(w\) of \(B\) lying above \(v\).
This is a standard fact about Dedekind domains. The key input is mathlib’s theorem primesOver_finite.
We write \(w|v\) to denote the fact that \(w\) is a prime of \(B\) above \(v\) of \(A\).
The product of the maps \(K_v\to L_w\) for \(w|v\) is a natural ring map \(K_v\to \prod _{w|v}L_w\) lying over \(K\to L\).
Because \(K_v\to \prod _{w|v}L_w\) lies over \(K\to L\), there’s an induced \(L\)-algebra map \(L\otimes _KK_v\to \prod _{w|v}L_w\). We are now able to state one of the key results in this section. The proof is probably the hardest proof in this section to formalize.
The induced \(L\)-algebra homomorphism \(L\otimes _KK_v\to \prod _{w|v}L_w\) is an isomorphism of rings.
My current proposal to formalize this is as follows. The map is surjective because the image is dense and closed; this has been formalized already. It is also a \(K_v\)-algebra homomorphism if we give \(L_w\) the obvious \(K_v\)-algebra structure. Thus we can conclude the result if we can prove that both spaces are finite-dimensional and have the same dimension. The \(K_v\)-dimension of \(L\otimes _KK_v\) is equal to the \(K\)-dimension of \(L\), which is \(\sum _{w|v}e_wf_w\) using the standard notation that \(e_w\) is the ramification index of \(w\) and \(f_w\) the residue degree (this result is in mathlib). So it suffices to prove that \([L_w:K_v]=e_wf_w\). We already have that \(e_w\) (defined globally) is equal to the local ramification index (defined as the factor by which the valuations differ on \(K\)). So what is left is to prove that (i) the residue field extension induced by \(L_w/K_v\) has degree is equal to the globally-defined \(f_w\), (ii) an extension of local fields has degree \(ef\). Now (i) sounds straightforward given what we have (the map from \(A\) to \(\mathcal{O}_v\) has kernel \(v\) and dense image) and (ii) is true for any complete discretely-valued field; I am not suggesting we formalize the following proof, but at least it represents a rigorous justification: A field complete with respect to a discrete valuation is stable in the sense of the book by Bosch-Güntzer-Remmert (Prop 3.6.2.1), so every finite extension of such a field is cartesian (def 3.6.1.1) and thus \(ef=n\) (Prop 3.6.2.4, (iii) implies (ii)). Note that if you weaken the hypotheses too much then there are counterexamples; it’s possible to have \(ef{\lt}n\) and BGR goes into details.
For \(v\) fixed, the product topology on \(\prod _{w|v}L_w\) is the \(K_v\)-module topology.
This is a finite product of \(K_v\)-modules each of which has the \(K_v\)-module topology by 8.7, and the product topology is the module topology for a finite product of modules each of which has the module topology (this is in mathlib).
If we give \(L\otimes _KK_v\) the \(K_v\)-module topology then the \(L\)-algebra isomorphism \(L\otimes _K K_v\cong \prod _{w|v}L_w\) is also a homeomorphism.
Indeed, is a \(K_v\)-algebra isomorphism between two modules each of which have the module topology, and any module map is automorphically continuous for the module topologies.
We now start thinking about what’s going on at the integral level. We write \(A_v\) for the integers of \(K_v\) and \(B_w\) for the integers of \(L_w\).
The isomorphism \(L\otimes _KK_v\to \prod _{w|v}L_w\) induces an isomorphism \(B\otimes _AA_v\to \prod _{w|v}B_w\) for all \(v\) in the height one spectrum of \(A\).
Certainly the image of the integral elements are integral. The argument in the other direction is more delicate. My original plan was to follow Cassels–Froehlich, Cassels’ article “Global fields”, section 12 lemma, p61, which proves it for all but finitely many primes, but a PR by Matthew Jasper gives another approach which works for all primes. Jasper’s argument is to show that the closure of \(A\) in \(K_v\) is \(A_v\) for a valuation on a Dedekind domain, and then that the closure of \(A\) in \(\prod _{v\in S}K_v\) is \(\prod _{v\in S}A_v\) for \(S\) a finite set of valuations (using the Chinese remainder theorem). Applying this to \(B\) we get that the closure of \(B\) in \(\prod _{w|v}L_w\) is \(\prod _{w|v}B_w\). He then shows that this closure is the image of \(B\otimes _A\mathcal{O}_v\) (by showing that this image is closed because it’s open), giving surjectivity; injectivity follows from the statement that \(L\otimes _KK_v=\prod _{w|v}L_w\).
A summary of what we have so far: for all finite places \(v\) of \(A\) we have shown that the natural map \(L\otimes _KK_v\to \prod _wL_w\) is an isomorphism of \(L\)-algebras, and that if \(L\otimes _KK_v\) has the \(K_v\)-module topology and each \(L_w\) has the valuation topology then this map is also a homeomorphism. Furthermore we have shown that there is an induced algebraic isomorphism \(B\otimes _AA_v\equiv \prod _w B_w\) on the subrings of the left and right hand sides.
Recall that the finite adeles \(\mathbb {A}_{A,K}^\infty \) is defined in mathlib to be the restricted product of the \(K_v\) with respect to the \(A_v\), equipped with a certain restricted product topology (which is not the subspace topology of the product topology, indeed \(\prod _v A_v\) is open in this topology). We have seen in definition 8.4 that there’s a map \(K_v\to L_w\) if \(w|v\), extending \(K\to L\), and we have seen in theorem 8.6 that this sends \(A_v\) to \(B_w\). We conclude
There’s a natural ring homomorphism \(\mathbb {A}_{A,K}^\infty \to \mathbb {A}_{B,L}^\infty \) lying over \(K\to L\).
Hence there’s a natural \(L\)-algebra homomorphism \(L\otimes _K\mathbb {A}_{A,K}^\infty \to \mathbb {A}_{B,L}^\infty \).
Our next goal in this section is the following two results. First the algebraic claim:
This natural map \(L\otimes _K\mathbb {A}_{A,K}^\infty \to \mathbb {A}_{B,L}^\infty \) is an isomorphism.
Now \(L\otimes _K\mathbb {A}_{A,K}^\infty \) is an \(\mathbb {A}_{A,K}^\infty \)-module and hence can be given the \(\mathbb {A}_{A,K}^\infty \)-module topology. We also claim
The induced \(L\)-algebra morphism \(L\otimes _K\mathbb {A}_{A,K}^\infty \to \mathbb {A}_{B,L}^\infty \) is a topological isomorphism.
Informally, the proofs are simple: componentwise we know that \(L\otimes _KK_v\) is isomorphic both algebraically and topologically to \(\prod _{w|v}L_w\), and that this isomorphism sends the open set \(B\otimes _AA_v\) homeomorphically onto \(\prod _{w|v}B_w\), so now it’s “just a case of putting everything together”. Formally, we really need to spell this out, as there is a lot going on. We do this in the next subsection.
8.4.2 Base change for nonarchimedean completions.
As usual we are in the AKLB set-up, so in particular \(K\) is the field of fractions of the Dedekind domain \(A\), \(L/K\) is a finite separable extension, and \(B\) is the integral closure of \(A\) in \(L\). The goal in this subsection is to spell out the following argument: Assume that \(L\otimes _KK_v\cong \prod _{w|v}L_w\) algebraically and topologically for all \(v\), with \(B\otimes _AA_v\) identified with \(\prod _{w|v}B_w\). Then \(L\otimes _K\mathbb {A}_K^\infty \cong \mathbb {A}_L^\infty \), algebraically and topologically. Here the tensor products \(L\otimes _K R\) (for \(R\) a \(K\)-algebra with a topology) are all being given the \(R\)-module topology, which if we choose a basis for \(L/K\) is just the product topology.
We start with the following observation. If \(M\) is a \(K\)-module then there’s a canonical map \(B\otimes _AM\to L\otimes _KM\) sending \(b\otimes m\) to \(b\otimes m\) (this follows from the universal property of the tensor product). Our first goal is to show that this map is an isomorphism. Let us establish some lemmas first.
If \(0\not=b\in B\) then there exists \(0\not=a\in A\) such that \(b\) divides the image of \(a\) in \(B\).
Is this already in mathlib?
Let \(a=N_{L/K}(b)\), the norm. This is known to take nonzero elements of \(L\) to nonzero elements of \(K\) (because the norm is the determinant of an invertible linear map) and integral elements to integral elements. Furthermore \(a/b\in L\) is the the product of the conjugates of \(b\) in some normal closure of \(L\), and hence it is integral, and thus in \(B\).
The \(A\)-bilinear map \(B\times K\to L\) sending \((b,k)\) to \(bk\) is surjective.
Given \(\lambda \in L\) write it as \(n/d\) with \(0\not=d\in B\). Choose \(0\not=a\in A\) and \(b\in B\) with \(db=a\) and then note \(\lambda =nb/a=nb\times a^{-1}\).
The natural map \(B\otimes _AK\to L\) is a \(B\)-algebra isomorphism.
We write down an inverse. Regard \(B\otimes _AK\) as a \(B\)-algebra via the action on the left. Note that at this point it’s not even clear that \(B\otimes _AK\) is a field. We have the structure map \(B\to B\otimes _AK\) sending \(b\) to \(b\otimes 1\), which is \(B\)-linear. I claim that every nonzero element of \(B\) gets sent to an invertible element of \(B\otimes _AK\). Indeed, if \(b\not=0\) and (using the previous lemma) we choose \(0\not=a\in A\) such that \(bb'=a\), then \((b\otimes 1)(b'\otimes \frac1a)=1\). Thus by the universal property of localisation, the \(B\)-linear map \(B\to B\otimes _AK\) extends to a ring homomorphism from the field of fractions of \(B\) to \(B\otimes _AK\), which we claim is our desired inverse. Checking that both composites are the identity should be straightforward. Starting with \(B\otimes _AK\) we only have to check on elements of the form \(b\otimes k\); starting with \(L\) we only have to check on elements of \(B\). Hopefully both are straightforward.
If \(M\) is any \(K\)-module then the canonical map \(B\otimes _A M\to L\otimes _K M\) is an isomorphism.
We can factor this map as \(B\otimes _AM\cong B\otimes _A(K\otimes _KM)\cong (B\otimes _A K)\cong _KM\to L\otimes _KM\) and we just showed that the latter map was an isomorphism.
We now need to explain how tensor products sometimes commute with restricted products. Something we will need along the way is
\(B\) is a finitely-presented \(A\)-module.
\(A\) is Noetherian as it is a Dedekind domain, so it suffices to prove that \(B\) is finitely-generated as an \(A\)-module. But this is in mathlib already (a proof is around line 101 of BaseChange.lean in FLT at the time of writing).
The reason we care about this is the following.
If \(R\) is a commutative ring, if \(M\) is a finitely presented \(R\)-module and if \(N_i\) are a collection of \(R\)-modules, then the canonical map \(M\otimes _R\prod _i N_i\to \prod _i(M\otimes _R N_i)\) is an isomorphism.
If \(M\) is finite and free then Maddy Crim has already formalized this in FLT. For the general case present \(M\) as \(R^a\to R^b\to M\to 0\) and use that tensor products and arbitrary products preserve surjections.
If \(S\) is a finite set of nonzero primes of \(A\) then the natural map \(B\otimes ((\prod _{v\in S}K_v)\times (\prod _{v\notin S}A_v))\to (\prod _{v\in S}(B\otimes _AK_v))\times (\prod _{v\notin S}(B\otimes _AA_v))\) is an isomorphism.
Follows from the previous two theorems.
Recall that \(\mathbb {A}_K^\infty \) is the finite adeles of \(K\), defined as the restricted product of the \(K_v\) with respect to the \(A_v\), where \(v\) runs through the nonzero primes of \(A\). Let \(R\) denote the restricted product of the \(B\otimes _A K_v\) with respect to the \(B\otimes _A A_v\).
The natural map \(B\otimes _A\mathbb {A}_K^\infty \to R\) is a \(B\)-algebra isomorphism.
This follows from the previous corollary and the fact that tensor products commute with filtered colimits.
Recall from earlier in this section that if \(v\) is a finite place of \(A\) then the natural map from \(B\otimes _A K_v\) to \(L\otimes _KK_v\) is an isomorphism, and recall from the previous section that the natural map from \(L\otimes _KK_v\) to \(\prod _{w|v}L_w\) was also an isomorphism. This isomorphism sends \(B\otimes _A A_v\) to \(\prod _{w|v}B_w\) (I thank Matthew Jasper for pointing out to me that this statement was true at all primes, not just at unramified primes). Finally, the set of \(w\) of \(B\) dividing a fixed place \(v\) of \(A\) is finite. Let’s now formalize the abstract statement which we need. Rather than following the notation for restricted product in the literature and writing \(\mathbb {A}_K^\infty =\prod '_vK_v\) with the \(\mathcal{O}_v\) implicit, we will write \(\prod '_v(K_v,\mathcal{O}_v)\) in the below.
Let \(V\) and \(W\) be index sets, and let \(f:W\to V\) be a map with finite fibres. Let \(X_v\) be sets, with subsets \(C_v\), let \(Y_w\) be sets with subsets \(D_w\), and say for all \(v\in V\) we’re given a bijection \(X_v\to \prod _{w|f(w)=v}Y_w\), identifying \(C_v\) with \(\prod _{w:f(w)=v}D_w\). Then there’s an induced bijection between the restricted products \(\prod '_v(X_v,C_v)\) and \(\prod '_w(Y_w,D_w)\).
The ring \(R\) introduced above (the restricted product of the \(B\otimes _A K_v\) with respect to the \(B\otimes _A A_v\)) is isomorphic to \(\mathbb {A}_L\).
Let \(V\) be the finite places of \(K\) and \(W\) the finite places of \(L\), let \(X_v\) be \(B\otimes _A K_v\), let \(C_v\) be \(B\otimes _A A_v\), let \(Y_w\) be \(L_w\), let \(D_w\) be \(B_w\) and the result follows from the previous definition, given theorem 8.13.
From this, we can deduce the theorem we claimed earlier:
The natural map \(B\otimes _A\mathbb {A}_K^\infty \to \mathbb {A}_L^\infty \) is a \(B\)-algebra isomorphism.
This map factors through the auxiliary ring \(R\) so the result follows from the previous two constructions.
Because this map factors through the isomorphism \(B\otimes _A\mathbb {A}_K^\infty \to L\otimes _K\mathbb {A}_K^\infty \) we can finally deduce that the natural map \(L\otimes _K\mathbb {A}_K^\infty \to \mathbb {A}_L^\infty \) is an algebraic isomorphism.
We still need to talk about topologies though, so let’s finish by doing this. Let’s start with some trivialities, expressed as definitions rather than theorems because they’re constructions.
If \(X_v\) and \(Y_v\) are families of topological spaces indexed by \(v\in V\), if \(f_v:X_v\to Y_v\) is a continuous map sending the subset \(C_v\subseteq X_v\) into \(D_v\subseteq Y_v\) then there’s an induced continuous map \(\prod '_v(X_v,C_v)\to \prod '_v(Y_v,D_v)\).
If all the \(f_v\) are homeomorphisms identifying \(C_v\) with \(D_v\) then the induced map on restricted products is also a homeomorphism (proof: apply the previous construction to \(f_v\) and their inverses)
We now allow a slight change of index set. Unfortunately I don’t think that we can deduce the results just stated above from this one, in Lean, because the product of \(Y_w\) over a set of size 1 is not definitionally equal to \(Y_w\).
Recall definition 8.26, giving us a bijection between two restricted products.
In the same setup as definition 8.26 (\(V,W\) index sets, \(f:W\to V\), \(C_v\subseteq X_v\) and \(D_w\subseteq Y_w\), bijections \(b_v:X_v\to \prod _{w:f(w)=v}Y_w\) identifying \(C_v\) with \(\prod _{w:f(w)=v}D_w\)), if all the \(X_v\) and \(Y_w\) are furthermore topological spaces, all the \(C_v\) and \(D_w\) are open, and all the \(b_v\) are homeomorphisms, then the induced map \(\prod '_v(X_v,C_v)\to \prod '_w(Y_w,D_w)\) is also a homeomorphism.
I have only thought about the cofinite filter case, where this should follow easily from the definition of the topology.
\(\mathbb {\mathbb {A}_L^\infty }\) is homeomorphic to \(\prod _v(B\otimes _AK_v,B\otimes _AA_v)\).
Follows from the previous theorem with \(X_v=B\otimes _AK_v\) \(D_w=L_w\) etc.
Recall that if
is a commutative ring, and two
-modules both have the
-module topology, then any
-linear morphism between them is automatically continuous. We know that \(\mathbb {A}_L^\infty \) is \(\mathbb {A}_K^\infty \)-linearly isomorphic to \(L\otimes _K\mathbb {A}_K^\infty \) and our claim is that if \(L\otimes _K\mathbb {A}_K^\infty \) is given the \(\mathbb {A}_K^\infty \)-module topology then this isomorphism is also a homeomorphism; to prove this, we thus just need to check that \(\mathbb {A}_L^\infty \) has the \(\mathbb {A}_K^\infty \)-module topology. Equivalently, by the previous result, we need to check that the restricted product topology on the \(\mathbb {A}_K^\infty \)-algebra \(\prod '_v(B\otimes _AK_v,B\otimes _AA_v)\) is the \(\mathbb {A}_K^\infty \)-module topology.
We now need to make restricted products of modules into modules over restricted product of rings. The API, which should be straightforward so we don’t give details here, is: if \(R_v\) are rings with subrings \(S_v\) and if \(M_v\) are \(R_v\)-modules with \(S_v\)-stable submodules \(N_v\), then \(\prod '_v(M_v,N_v)\) is naturally a module over \(\prod '_v(R_v,S_v)\), and that \(R_v\)-morphisms \(M_v\to M_v'\) sending \(N_v\) to \(N_v'\) induce \(\prod '_v(R_s,S_v)\)-linear maps \(\prod '_v(M_v,N_v)\to \prod '_v(M'_v,N'_v)\). From this one deduces that isomorphisms on the factors induce isomorphisms on the restricted products.
Now \(A_v\) is a PID, so \(B\otimes _AA_v\) is free (as it is finitely-generated and torsion-free). This means that there is an isomorphism \(B\otimes _AA_v\cong (A_v)^n\), which extends to an isomorphism \(B\otimes _AK_v\cong K_v^n\). These isomorphisms are also homeomorphisms. If we fix such isomorphisms for all \(v\) then we get an induced \(\mathbb {A}_K^\infty \)-module isomorphism + homeomorphism \(\prod '_v(B\otimes _AK_v,B\otimes _AA_v)=\prod '_v(K_n^n,A_v^n)\). So it suffices to prove that the \(\prod '_v(K_v,A_v)\)-module \(\prod '_v(K_v^n,A_v^n)\) has the \(\prod '_v(K_v,A_v)\)-module topology. This follows from the fact that the product topology on two modules with the module topology is the module topology (a fact in mathlib) and the following result.
If \(X_v\) and \(Y_v\) are topological spaces with open subspaces \(C_v\) and \(D_v\), then the obvious bijection \(\prod '_v(X_v \times Y_v,C_v\times D_v) \cong \left(\prod '_v(X_v,C_v)\right)\times \left(\prod '_v(Y_v,D_v)\right)\) is a homeomorphism, where the restricted products have the restricted product topology and the binary product has the product topology.
This should hopefully be straightforward using RestrictedProduct.continuous_dom_prod
As a corollary one can prove by induction on \(n\) that the restricted product of \(n\)th powers is homeomorphic to the \(n\)th power of the restricted product and this is the result we require.
8.4.3 Base change for infinite adeles
Recall that if \(K\) is a number field then the infinite adeles of \(K\) are defined to be the product \(\prod _{v\mid \infty } K_v\) of all the completions of \(K\) at the infinite places.
The result we need here is that if \(L/K\) is a finite extension of number fields, then the map \(K\to L\) extends to a continuous \(K\)-algebra map \(K_\infty \to L_\infty \), and thus to a continuous \(L\)-algebra isomorphism \(L\otimes _KK_\infty \to L_\infty \). Perhaps a cheap proof would be to deduce it from the fact that \(K_\infty =K\otimes _{\mathbb {Q}}\mathbb {R}\).
The overall strategy is to first establish, for each infinite place \(v\) of \(K\), homeomorphisms between for the completion \(K_v\) and the product \(\prod _{w\mid v}L_w\) of completions of \(L\) at all infinite places \(w\) of \(L\) lying above \(v\). We then use these homeomorphisms to construct base change for the infinite adele ring.
Weak approximation at infinite places
First, we require a preliminary result that \(K\) is dense inside any product of completions \(\prod _{v\in S} K_v\) of \(K\) at infinite places.
Let \(S\) be a set of infinite places of \(K\). The image of \(K\) under the embedding \(K\hookrightarrow (K_v)_{v\in S}; k \mapsto (k)_v\) is dense in the product topology.
Let \((K, v)\) denote \(K\) equipped with the topology induced by the infinite place \(v\). It suffices to show that the image of \(K\) under the embedding \(K\hookrightarrow \prod _{v\mid \infty }(K, v)\) is dense in the product topology. By a standard analytic argument, for each \(v\) it is possible to select a sequence \((x_n^{(v)})_n\) with the property that \(x_n^{(v)} \to 1\) in \(v\)’s topology, while \(x_n^{(v)} \to 0\) in any other infinite place’s topology. Let \((z_v)_v \in \prod _{v\mid \infty }(K, v)\). For each \(v\), the sequence \(y_n := \sum _{v\mid \infty } x_n^{(v)}z_v\) in \(K\) converges to \(z_v\) in \(v\)’s topology. So the embedded image of \(y_n\) in \(\prod _{v\mid \infty }(K, v)\) converges to \((z_v)_v\) in the product topology.
Dimensionality of \(\prod _{w\mid v}L_w\) as a \(K_v\)-vector space
This subsection contains a result that the \(K_v\)-dimension of \(L \otimes _K K_v\) is equal to the \(K_v\)-dimension of \(\prod _{w\mid v}L_w\).
For a fixed infinite place \(v\) of \(K\), we have \(\text{dim}_{K_v} \prod _{w\mid v} L_w = \text{dim}_{K_v} L\otimes _K K_v\).
Base change at infinite places
Let \(v\) be an infinite place of \(K\). There is a continuous \(K\)-algebra homomorphism \(K_v \to \prod _{w\mid v}L_w\), whose restriction to \(K\) corresponds to the global embedding of \(K\) into \((L_w)_w\).
The map in 8.36 can be lifted to an \(L\)-algebra homomorphism defined on \(L\otimes _K K_v\).
Let \(v\) be an infinite place of \(K\). There is a natural \(L\)-algebra homomorphism \(L\otimes _K K_v \to \prod _{w\mid v}L_w\), whose restriction to \(1\otimes _K K_v\) corresponds to the map in 8.36.
For a fixed infinite place \(v\) of \(K\), the map \(L\otimes _K K_v \to \prod _{w\mid v}L_w\) is surjective.
Let \((x_i)_i\) be a \(K_v\)-basis of \(\prod _{w\mid v}L_w\). By the density of \(L\) in \(\prod _{w\mid v}L_w\) (Theorem 8.34), we can find \(\alpha _i \in L\) arbitrarily close to \(x_i\prod _{w\mid v}L_w\) with respect to the sup norm when embedded globally in \(\prod _{w\mid v}L_w\). In particular, it is possible to choose such \(\alpha _i\) so that the matrix representing the vector \(((\alpha _i)_{w \mid v})_i\) in the basis \((x_i)_i\) has non-zero determinant. Since \((\alpha _i)_{w \mid v}\) is the image of \(1\otimes \alpha _i\) under base change, we have that \((1 \otimes \alpha _i)_i\) also forms a basis of \(L\otimes _K K_v\), and base change is surjective.
For a fixed infinite place \(v\) of \(K\), the map \(L\otimes _K K_v \to \prod _{w\mid v}L_w\) is injective.
We have established that the map of Definition 8.37 gives an \(L\)-algebra isomorphism between \(L\otimes _K K_v\) and \(\prod _{w\mid v}L_w\). The left-hand side is given the \(K_v\)-module topology, while we show that the right-hand side also has the \(K_v\)-module topology.
If \(w \mid v\) is an infinite place of \(L\) lying above the infinite place \(v\) of \(K\), then \(L_w\) has the \(K_v\)-module topology.
Because \(L_w\) is a finite-dimensional normed \(K_v\) vector space, there exists a \(K_v\)-linear linear homeomorphism \(L_w \cong K_v^n\), from which \(L_w\) has the \(K_v\)-module topology.
Let \(v\) be an infinite place of \(K\). There is a natural \(L\)-algebra homeomorphism \(L\otimes _K K_v \cong _L \prod _{w\mid v}L_w\), whose restriction to \(1\otimes _K K_v\) corresponds to the map in 8.36.
The map in 8.37 is an \(L\)-algebra isomorphism by Theorem 8.38 and Theorem 8.39. Every \(K_v\)-algebra isomorphism between two \(K_v\)-module topological spaces is a homeomorphism. Since the \(L\)-algebra isomorphism of Definition 8.37 can equivalently be viewed as a \(K_v\)-algebra isomorphism, it is also a homeomorphism.
Let \(v\) be an infinite place of \(K\). There is a natural \(K_v\)-linear homeomorphism \(K_v^{[L:K]} \cong _{K_v} \prod _{w\mid v}L_w\).
Compose the \(K_v\)-linear isomorphism \(K_v^{[L:K]} \cong \prod _{w\mid v}L_w\) with the \(K_v\)-linear version of base change 8.41 to get the isomorphism in the statement. Since both sides have the \(K_v\)-module topology, then this is also a homeomorphism.
Base change for the infinite adele ring
First, we induce a \(K_{\infty }\)-algebra on \(L_{\infty }\) from the action of each \(K_v\) on \(\prod _{w\mid v}L_w\). Specifically, this means that for \(x \in K_{\infty }\) and \(y \in L_{\infty }\), we have \((x \cdot y)_w = x_{v_w} \cdot y_w\), where \(v_w\) is the restriction of \(w\) to \(K\). We show that \(L_{\infty }\) has the \(K_{\infty }\)-module topology.
There is a natural \(K_{\infty }\)-linear homeomorphism \(K_{\infty }^{[L:K]} \cong _{K_{\infty }} L_{\infty }\).
Using the isomorphisms \(K_v^{[L:K]} \cong _{K_v} \prod _{w\mid v}L_w\) from Theorem 8.42, we clearly have a bijection \(K_{\infty }^{[L:K]} \cong \prod _v\prod _{w \mid v} L_w \cong \prod _w L_w\). The \(K_v\)-linearity of each component isomorphism extends to \(K_{\infty }\)-linearity if the action of \(\prod _v K_v\) on \(\prod _w L_w\) is constant on the fibers of the restriction map on infinite places. In other words, if, for all \(x \in K_{\infty }\) and \(y \in L_{\infty }\), we have \((x \cdot y)_w = x_{v_w} \cdot y_w\), which is true by definition.
\(L_{\infty }\) has the \(K_{\infty }\)-module topology.
Since \(L_{\infty }\) is homeomorphic to a finite product of \(K_{\infty }\) as a \(K_{\infty }\)-vector space, it has the \(K_{\infty }\)-module topology.
There is a natural \(L\)-algebra isomorphism \(L \otimes _K K_{\infty } \cong _L L_{\infty }\).
This follows from the following chain of isomorphisms:
The first isomorphism is the standard \(L\)-algebra isomorphism \(L \otimes _K \prod _v K_v \cong _L \prod _v (L \otimes _K K_v)\). The second isomorphism is given by the component \(L\)-algebra isomorphisms \(L \otimes _K K_v \cong _L \prod _{w\mid v}L_w\) from Theorem 8.41.
It remains to show that the map in 8.45 is a homeomorphism. Since both sides have the \(K_{\infty }\)-module topology, and since the \(L\)-algebra isomorphism of 8.45 can equivalently be viewed as a \(K_{\infty }\)-linear isomorphism, it is also a homeomorphism.
If \(K\to L\) is a ring homomorphism between two number fields then there is a natural isomorphism (both topological and algebraic) \(L\otimes _KK_\infty \cong L_\infty \).
Since both sides of the \(L\)-algebra isomorphism in 8.45 have the \(K_{\infty }\)-module topology, and since the isomorphism can equivalently be viewed as a \(K_{\infty }\)-linear isomorphism, it is also a homeomorphism.
8.4.4 Base change for adeles
From the previous results we deduce immediately that if \(L/K\) is a finite extension of number fields then there’s a natural (topological and algebraic) isomorphism \(L\otimes _K\mathbb {A}_K\to \mathbb {A}_L\).
If \(K\to L\) is a ring homomorphism between two number fields then there is a natural isomorphism (both topological and algebraic) \(L\otimes _K\mathbb {A}_K\cong \mathbb {A}_L\).
Follows from the previous results.
Something else we shall need:
If \(K\to L\) is a ring homomorphism between two number fields then the topology on \(\mathbb {A}_L\) is the \(\mathbb {A}_K\)-module topology, where the module structure comes from the natural map \(\mathbb {A}_K\to \mathbb {A}_L\).
Indeed \(\mathbb {A}_L\cong L\otimes _K\mathbb {A}_K\) is a homeomorphism, and the right hand side has the \(\mathbb {A}_K\)-module topology.
8.5 Discreteness and compactness
We need that if \(K\) is a number field then \(K\subseteq \mathbb {A}_K\) is discrete, and the quotient (with the quotient topology) is compact. Here is a proposed proof.
There’s an open subset of \(\mathbb {A}_{\mathbb {Q}}\) whose intersection with \(\mathbb {Q}\) is \(\{ 0\} \).
Use \(\prod _p{\mathbb {Z}_p}\times (-1,1)\). Any rational \(q\) in this set is a \(p\)-adic integer for all primes \(p\) and hence (writing it in lowest terms as \(q=n/d\)) satisfies \(p\nmid d\), meaning that \(d=\pm 1\) and thus \(q\in \mathbb {Z}\). The fact that \(q\in (-1,1)\) implies \(q=0\).
There’s an open subset of \(\mathbb {A}_{K}\) whose intersection with \(K\) is \(\{ 0\} \).
By a previous result, we have \(\mathbb {A}_K=K\otimes _{\mathbb {Q}}\mathbb {A}_{\mathbb {Q}}\). Choose a basis of \(K/\mathbb {Q}\); then \(K\) can be identified with \(\mathbb {Q}^n\subseteq (\mathbb {A}_{\mathbb {Q}})^n\) and the result follows from the previous theorem.
The additive subgroup \(K\) of \(\mathbb {A}_K\) is discrete.
If \(x\in K\) and \(U\) is the open subset in the previous lemma, then it’s easily checked that \(K\cap U=\{ 0\} \) implies \(K\cap (U+x)=\{ x\} \), and \(U+x\) is open.
For compactness we follow the same approach.
The quotient \(\mathbb {A}_{\mathbb {Q}}/\mathbb {Q}\) is compact.
The space \(\prod _p\mathbb {Z}_p\times [0,1]\subseteq \mathbb {A}_{\mathbb {Q}}\) is a product of compact spaces and is hence compact. I claim that it surjects onto \(\mathbb {A}_{\mathbb {Q}}/\mathbb {Q}\). Indeed, if \(a\in \mathbb {A}_{\mathbb {Q}}\) then for the finitely many prime numbers \(p\in S\) such that \(a_p\not\in \mathbb {Z}_p\) we have \(a_p\in \frac{r_p}{p^{n_p}}+\mathbb {Z}_p\) with \(r_p/p^{n_p}\in \mathbb {Q}\), and if \(q=\sum _{p\in S}\frac{r_p}{p^{n_p}}\in \mathbb {Q}\) then \(a-q\in \prod _p\mathbb {Z}_p\times \mathbb {R}\). Now just subtract \(\lfloor a_{\infty }-q\rfloor \) to move into \(\prod _p\mathbb {Z}_p\times [0,1)\) and we are done.
The quotient \(\mathbb {A}_K/K\) is compact.
We proceed as in the discreteness proof above, by reducing to \(\mathbb {Q}\). As before, choosing a \(\mathbb {Q}\)-basis of \(K\) gives us \(\mathbb {A}_K/K\cong (\mathbb {A}_{\mathbb {Q}}/\mathbb {Q})^n\) so the result follows from the previous theorem.