\(\widehat{\mathbb{Z}}\)
Classically automorphic forms were defined as functions on symmetric spaces (like the upper half plane) which transformed well under the action of certain discrete groups (for example \(\operatorname{SL}_2(\mathbb{Z})\)). However such definitions became combinatorially problematic when generalised to number fields with nontrivial class group, because the classical theory needed a number \(p\) to define the Hecke operator \(T_p\), and in the case where \(p\) was a non-principal prime ideal in a number field, there was no appropriate number. One fix is to take disjoint unions of symmetric spaces indexed by the ideal class group of the field in question, but it is easier to work adelically, which is morally what we shall do. However we are able to avoid introducing the adeles explicitly; we can work instead with the conceptually simpler object \(\widehat{\mathbb{Z}}\), the profinite completion of \(\mathbb{Z}\). So what is \(\widehat{\mathbb{Z}}\)? We offer a low-level definition of this object.
Given an integer \(z\), we can reduce it mod \(N\) for every positive natural number and get elements \(z_N=\overline{z}\in\mathbb{Z}/N\mathbb{Z}\). These elements are not completely arbitrary though – they must satisfy some compatibility conditions. For example there can be no positive integer \(z\) such that \(z_{10}=6\) and \(z_2=1\), because \(z_{10}=6\) tells us that \(z\) ends in a 6 when written in base 10, and in particular it's even, so \(z_2\) must be 0. The general rule: if \(D\mid N\) then \(z_D\) must be equal to image of \(z_N\) under the natural ring homomorphism from \(\mathbb{Z}/N\mathbb{Z}\) to \(\mathbb{Z}/D\mathbb{Z}\). We say that a collection of elements \(z_N\in\mathbb{Z}/N\mathbb{Z}\) is compatible if it satisfies this rule.
DefinitionZHat#
The profinite completion \(\widehat{\mathbb{Z}}\) of \(\mathbb{Z}\) is the set of all compatible collections \(c=(c_N)_N\) of elements of \(\mathbb{Z}/N\mathbb{Z}\) indexed by \(\mathbb{N}^+:=\{1,2,3,\ldots\}\). A collection is said to be compatible if for all positive integers \(D\mid N\), we have \(c_N\) mod \(D\) equals \(c_D\).
Used by 3
LemmaZHat.commRing#
\(\widehat{\mathbb{Z}}\) is a subring of \(\prod_{N\geq1}(Z/N\mathbb{Z})\) and in particular is a ring.
Uses 1 · Used by 11
Examples of elements of \(\widehat{\mathbb{Z}}\) are are given by integers, where we define \(z_N\) to be \(z\) mod \(N\) for all \(N\). This gives us a natural map from \(\mathbb{Z}\) to \(\widehat{\mathbb{Z}}\). In particular we can talk about \(0\in\widehat{\mathbb{Z}}\) and \(1\in\widehat{\mathbb{Z}}\).
LemmaZHat.nontrivial#
\(0\not=1\) in \(\widehat{\mathbb{Z}}\).
Proof
Recall that you can evaluate an element of \(\widehat{\mathbb{Z}}\) at a positive integer. Evaluating \(0\) at 2 gives \(0\), and evaluating \(1\) at \(2\) gives \(1\), and these are distinct elements of \(\mathbb{Z}/2\mathbb{Z}\), so \(0\not=1\) in \(\widehat{\mathbb{Z}}\).
Lean
Formalized as ZHat.nontrivial.
Sources
Uses 1
LemmaZHat.charZero#
The map from the naturals into \(\widehat{\mathbb{Z}}\) sending \(n\) to \(n\) is injective.
Proof
Generalise the above idea. Feel free to write up a LaTeX proof and PR it.
Lean
Formalized as ZHat.charZero.
Sources
Used by 1
Note that it follows easily that that the map from the integers to \(\widehat{\mathbb{Z}}\) is injective.
But \(\widehat{\mathbb{Z}}\) is much larger than \(\mathbb{Z}\); it has the same cardinality as the reals in fact. Let's write down an explicit example of an element of \(\widehat{\mathbb{Z}}\) which isn't obviously in \(\mathbb{Z}\).
DefinitionZHat.e#
The infinite sum \(0!+1!+2!+3!+4!+5!+\cdots\) looks like it makes no sense at all; it is the sum of an infinite series of larger and larger positive numbers. However, the sum is finite modulo \(N\) for every positive integer \(N\), because all the terms from \(N!\) onwards are multiples of \(N\) and thus are zero in \(\mathbb{Z}/N\mathbb{Z}\). Thus it makes sense to define \(e_N\) to be the value of the finite sum modulo \(N\). Explicitly, \(e_N=0!+1!+\cdots+(N-1)!\) modulo \(N\).
Uses 1 · Used by 2
LemmaZHat.e_def#
The collection \((e_N)_N\) is an element of \(\widehat{\mathbb{Z}}\).
Proof
This boils down to checking that \(D!+(D+1)!+\cdots+(N-1)!\) is a multiple of \(D\).
Lean
Formalized as ZHat.e_def.
Sources
Uses 1
LemmaZHat.e_not_in_Int#
The element \((e_N)_N\) of \(\widehat{\mathbb{Z}}\) is not in \(\mathbb{Z}\).
Proof
First imagine that \(e=n\) with \(n\in\mathbb{Z}\) and \(0\leq n\). In this case, choose \(j\) such that \(0!+1!+2!+\cdots+j!>n\) and check also that the sum is less than \((j+1)!\). Now set \(N=(j+1)!\) and let's compare \(e_N\) and \(n_N=n\). The trick is that \(e_N\) must be \(0!+1!+\cdots+j!\) mod \(N\), because all the terms beyond this are multiples not just of \((j+1)\) but of \((j+1)!=N\). Thus mod \(N\) we have \(0\leq n\lt e_N\lt N\) so \(n\not=e\).
Now we deal with \(n=-t<0\); choose \(j\) large such that \((j+1)!-(0!+1!+\cdots+j!)>t\) (possible because the sum is at most \(2\times j!\)) and then set \(N=(j+1)!\) and we have \(0 < e_N\lt N-t\lt N\) so we cannot have \(e_N=-t\) in \(\mathbb{Z}/N\mathbb{Z}\), so again \(e\not=n\).
Lean
Formalized as ZHat.e_not_in_Int.
Sources
Uses 1
Let's prove some more basic facts about \(\widehat{\mathbb{Z}}\).
LemmaZHat.torsionfree#
If \(0\lt N\) is an integer then multiplication by \(N\) is injective on \(\widehat{\mathbb{Z}}\).
Proof
Suppose that \((z_i)_i\in\widehat{\mathbb{Z}}\) and \(Nz=0\). This means that \(Nz_i=0\in\mathbb{Z}/i\mathbb{Z}\) for all \(i\). Let us fix an arbitrary positive integer \(j\); we need to prove that \(z_j=0\in\mathbb{Z}/j\mathbb{Z}\). Consider the element \(z_{Nj}\in\mathbb{Z}/Nj\mathbb{Z}\). By assumption, we have \(Nz_{Nj}=0\), meaning that if we lift \(z_{Nj}\) to an integer, we have \(Nj\mid Nz_{Nj}\), and thus \(j\mid z_{Nj}\). Thus by the compatibility assumption on the \(z_i\) we have that \(z_j\in\mathbb{Z}/j\mathbb{Z}\) is the mod \(j\) reduction of \(z_{Nj}\) and hence is zero.
Lean
Formalized as ZHat.torsionfree.
Sources
Uses 2 · Used by 1
We will also need to understand exactly which elements of \(\widehat{\mathbb{Z}}\) are multiples of \(N\).
LemmaZHat.multiples#
The multiples of \(N\) in \(\widehat{\mathbb{Z}}\) are precisely the compatible collections \((z_i)_i\in\widehat{\mathbb{Z}}\) with \(z_N=0\).
Proof
Clearly \(z_N=0\) is a necessary condition to be a multiple of \(N\). To see it is sufficient, take a general \((z_i)\in\widehat{\mathbb{Z}}\) such that \(z_N=0\), and now define a new element \((y_j)_j\) of \(\widehat{\mathbb{Z}}\) by \(y_j=z_{Nj}/N\). Just to clarify what this means: \(z_{Nj}\in\mathbb{Z}/Nj\mathbb{Z}\) reduces mod \(N\) to \(z_N=0\) by the compatibility assumption, so it is in the subgroup \(N\mathbb{Z}/Nj\mathbb{Z}\) of \(\mathbb{Z}/Nj\mathbb{Z}\), which is isomorphic (via "division by \(N\)") to the group \(\mathbb{Z}/j\mathbb{Z}\); this is how we construct \(y_j\). It is easily checked that the \(y_j\) are compatible and that \(Ny=z\).
Lean
Formalized as ZHat.multiples.
Sources
Uses 1 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.