Restricted products
In the concrete example of Hecke operators which we care about, the invariants \(A^G\) will be spaces of quaternionic automorphic forms (by definition). We do not need to worry about the definition of \(A\) in this project at all. However we will need to do various computations with the specific groups \(G\) which we are interested in, and they are restricted products. So we now develop some theory for restricted products, starting by recalling the definition.
If \(I\) is an index set, if \(X_i\) are sets indexed by \(i\in I\) and if \(Y_i\) are subsets, then the restricted product \(\prod'_iX_i\) (note the dash) is defined to be the subset of the full product \(\prod_i X_i\) consisting of those tuples \((x_i)\) such that \(x_i\in Y_i\) for all but finitely many \(i\). We suppress the \(Y_i\) from the notation in this document, although in Lean we cannot do this and the restricted product looks something like \(\prod{}^{r} i,[X\ i, Y\ i]\).
It is straightforward to check that if the \(X_i\) are groups or rings or \(R\)-modules, and the \(Y_i\) are subgroups or subrings or submodules, then the restricted product is a group, ring or \(R\)-module; indeed the structure is inherited via the inclusion \(\prod'_iX_i\subseteq\prod_iX_i\) (and the fact that arbitrary products of groups/rings/modules are groups/rings/modules).
More subtle is the theory of topological space structures. If the \(X_i\) are topological spaces then we do not give \(\prod'_iX_i\) the subspace topology coming from the product topology on \(\prod_iX_i\); instead we give it the finest topology making all of the natural maps \(\prod_{i\in S}X_i\times\prod_{i\notin S}Y_i\to \prod'_iX_i\) continuous, as \(S\) runs through all finite subsets of \(I\); here the product of \(X_i\)s and \(Y_i\)s has the product topology. For example if all of the \(Y_i\) are open then one can check that \(\prod_iY_i\) is an open subset of \(\prod'_iX_i\) (this is RestrictedProduct.isOpen_forall_mem in mathlib), whereas it is not of the form \(\left(\prod'_iX_i\right)\cap U\) for any open subset \(U\) of \(\prod_iX_i\) in general; the map from \(\prod'_i X_i\) to \(\prod_i X_i\) is continuous but is not in general an embedding.
If you've seen automorphic forms before, then here is an obvious-sounding claim: because the adeles \(\mathbb{A}_F\) of a number field are a restricted product of completions \(F_v\) with respect to the integer rings \(\mathcal{O}_v\), then \(GL_2(\mathbb{A}_F)\) is obviously topologically a restricted product of \(GL_2(F_v)\) with respect to \(GL_2(\mathcal{O}_v)\). We now spend some time justifying this claim, which is a little more intricate than it sounds.
Products
Here are some basic facts we need about restricted products.
LemmaHomeomorph.restrictedProductProd#
If \(A_i\) is a family of topological spaces equipped with open subsets \(B_i\), and if \(C_i\) is a family of topological spaces equipped with open subsets \(D_i\), and if we equip \(A_i\times C_i\) with the open subset \(B_i\times D_i\), then the natural bijection \(\prod'_i(A_i\times C_i)=\left(\prod'_iA_i\right)\times\left(\prod'_iB_i\right)\) is a homeomorphism.
Proof
We need to check continuity in both directions. The easy way is continuity of the map from the restricted product to the map from the binary product; the lemma RestrictedProduct.continuous_dom in mathlib tells us that a map from a restricted product is continuous when its restriction to \(\left(\prod_{i\in S}(A_i\times C_i)\right)\times\left(\prod_{i\notin S}(B_i\times D_i)\right)\) is continuous for all finite \(S\subseteq I\); the universal property of the binary product tells us that the map into the binary product is continuous iff the maps into the factors are continuous, but the map into \(\prod'_iX_i\) is a product of the natural maps from \(\left(\prod_{i\in S}(A_i\times C_i)\right)\times\left(\prod_{i\notin S}(B_i\times D_i)\right)\) to \(\left(\prod_{i\in S}A_i\right)\times\left(\prod_{i\notin S}B_i\right)\) and the inclusion, and both are known to be continuous (an arbitrary product of continuous maps is continuous, and the other claim is in the restricted product API in mathlib).
The harder direction is the other way, because we are working against both universal properties. The trick is RestrictedProduct.continuous_dom_prod in mathlib (this is where we assume \(B_i\) and \(D_i\) are open), which tells us that a map out of a binary product of restricted products is continuous when its restriction to \(\left(\left(\prod_{i\in S}A_i\right)\times\left(\prod_{i\notin S}B_i\right)\right)\times \left(\left(\prod_{i\in S}C_i\right)\times\left(\prod_{i\notin S}D_i\right)\right)\) is, for all finite \(S\) (note that the \(S\) in the mathlib lemma is actually our \(I-S\)). The map from this to the restricted product factors through \(\left(\prod_{i\in S}(A_i\times C_i)\right)\times\left(\prod_{i\notin S}(B_i\times D_i)\right)\); the first map is a homeomorphism (use the fact that \(\prod_iX_i\times Y_i\) is homeomorphic to \(\left(\prod_iX_i\right)\times\left(\prod_iY_i\right)\)), and the second is continuous by definition of the topology on a restricted product.
Lean
Formalized as Homeomorph.restrictedProductProd.
Sources
Used by 1
Remark. This may well not be true if \(B_i\) and \(D_i\) are not open, because filtered colimits and binary products do not appear in general to commute in the category of topological spaces. I don't know an explicit counterexample though.
The proof of Lemma Homeomorph.restrictedProductProd is shown with its statement.
CorollaryHomeomorph.restrictedProductPi#
Restricted products (with respect to open subspaces) commute with finite products. In other words, if \(j\) runs through a finite set \(J\) and \(i\) runs through an arbitrary set \(I\), and if \(X_{ji}\) are topological spaces equipped with open subspaces \(Y_{ji}\), then the obvious bijection \(\prod'_i(\prod_j X_{ji})=\prod_j\left(\prod'_i X_{ji}\right)\) is a homeomorphism.
Proof
Induction on the size of the finite set, using lemma Homeomorph.restrictedProductProd to get you started.
Lean
Formalized as Homeomorph.restrictedProductPi.
Sources
Uses 1 · Used by 1
Let \(n\) be a natural and let \(M_n(X)\) for a set \(X\) denote “\(n\times n\) matrices with coefficient in \(X\)”, i.e. \(X^{n^2}\). If \(X\) is a topological spaces then give \(M_n(X)\) the product topology.
CorollaryHomeomorph.restrictedProductMatrix#
If \(X_i\) are topological spaces and the \(Y_i\) are open subspaces, then the obvious map \(M_n(\prod'_iX_i)=\prod'_iM_n(X_i)\) is a homeomorphism.
Proof
Immediate from the previous corollary Homeomorph.restrictedProductPi.
Lean
Formalized as Homeomorph.restrictedProductMatrix.
Sources
Uses 1 · Used by 1
Units
We now want to move from matrices to invertible matrices whilst keeping track of topology, so we need to understand units of topological monoids. Openness of the subobject was crucial in the above arguments, so we need the next lemma before we can get anywhere.
LemmaSubmonoid.units_isOpen#
If \(M\) is a topological monoid and \(U\) is an open submonoid, then the units \(U^\times\) of \(U\) are naturally an open subgroup of \(M^\times\).
Proof
We have \(U\times U\) is an open subset of \(M\times M\), and if we imagine \(M^\times\) embedded in \(M\times M\) as explained in the remark above, then the intersection of this subgroup with \(U\times U\) is open in \(M^\times\) and consists of the elements of \(M^\times\) which are in \(U\) and whose inverse is also in \(U\), which is easily checked to be the copy of \(U^\times\) we're talking about.
Lean
Formalized as Submonoid.units_isOpen.
Sources
Used by 1
Remark. Note that \(M^\times\) doesn't get the subspace topology from \(M\), it is embedded into \(M\times M\) via \(g\mapsto (g,g^{-1})\) and gets the subspace topology from the product. This makes it into a topological group.
The proof of Lemma Submonoid.units_isOpen is shown with its statement.
Later on, compactness will be key for us, so we record the analogous result for compactness.
LemmaSubmonoid.units_isCompact#
If \(M\) is a Hausdorff topological monoid and \(U\) is a compact submonoid, then the units \(U^\times\) of \(U\) are naturally a compact subgroup of \(M^\times\).
Proof
First I claim that \(M^\times\) embedded in \(M\times M\) via \(g\mapsto (g,g^{-1})\) is a closed subset of \(M\times M\). Indeed, if \(p:M\times M\to M\) is \((a,b)\mapsto ab\) and \(q:M\times M\to M\) is \((a,b)\mapsto ba\), then \(p\) and \(q\) are continuous, \(M^\times\subseteq M\times M\) is the intersection \(p^{-1}\{1\}\cap q^{-1}\{1\}\), and \(\{1\}\) is closed because \(M\) is Hausdorff.
We have \(U\times U\) is a compact subset of \(M\times M\), and so \(U^\times=M^\times\cap U\times U\) is a closed subspace of a compact space and is thus compact.
Lean
Stated as Submonoid.units_isCompact; the blueprint marks no proof of it as formalized.
Sources
Remark. Is Hausdorffness necessary?
The proof of Lemma Submonoid.units_isCompact is shown with its statement.
LemmaContinuousMulEquiv.piUnits#
If \(U_i\) are topological monoids then the canonical group isomorphism \((\prod_i U_i)^\times=\prod_i(U_i^\times)\) is a homeomorphism.
Proof
We prove that the maps in both directions are continuous. Let's start with the map from left to right.
A map into a product is continuous when the maps to the factors are continuous. A map into the units of a monoid is continuous when the two projection maps to the monoid (the inclusion and the map \(u\mapsto u^{-1}\)) are continuous (because \(M^\times\) has the topology induced from \(M\times M\)). This reduces us to checking that the maps \((\prod_i U_i)^\times\to U_j\) sending \((u_i)\) to \(u_j\) resp \(u_j^{-1}\) are continuous. But the former map is the continuous inclusion \((\prod_i U_i)^\times\to\prod_i U_i\) followed by the continuous projection to \(U_j\), and the latter map is the continuous inclusion \((\prod_i U_i)^\times\to\prod_i U_i\) sending \(x\) to \(x^{-1}\) followed by the projection.
To go the other way: because the units have the induced topology it suffices to check that the two maps \(\prod_i(U_i^\times)\to\prod_i U_i\) sending \((u_i)\) to \((u_i)\) resp \((u_i^{-1})\) are continuous. A map to a product is continuous when the induced maps to the factors are. A projection from a project is continuous, and the identity and inverse are continuous maps \(U_j^\times\to U_j\), and the maps we're concerned with are composites of these maps and are hence continuous.
Lean
Formalized as ContinuousMulEquiv.piUnits.
Sources
Used by 1
TheoremContinuousMulEquiv.restrictedProductUnits#
If \(M_i\) are a family of topological monoids equipped with open submonoids \(U_i\), then the canonical map \((\prod'_iM_i)^\times\to\prod'_i(M_i^\times)\) is a homeomorphism.
Proof
I don't know a clean way of showing that the map from left to right is continuous, so here is a “direct” proof that the map is a homeomorphism. It is certainly an abstract group isomorphism between topological groups. So to prove that it is a homeomorphism it suffices to prove that it is a homeomorphism near the identity, or equivalently that there are open neighbourhoods \(X\) and \(Y\) of the identity elements on each side such that the map induces a homeomorphism from \(X\) to \(Y\). We choose \((\prod_i U_i)^\times\) and \(\prod_i (U_i^\times)\). Note that the former is open because of lemma Submonoid.units_isOpen. The result now follows from the previous lemma ContinuousMulEquiv.piUnits.
Lean
Formalized as ContinuousMulEquiv.restrictedProductUnits.
Sources
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.