Some local theory
We could work over a general nonarchimedean normed field but we still do not have them in mathlib, so we stick to the case of interest which is the completion of a number field \(K\) at a finite place \(v\). Such a completion is a topological field \(K_v\) equipped with a discrete valuation, a ring of integers \(\mathcal{O}_v\) having a principal maximal ideal \((\varpi)\), and a finite residue field \(k_v:=\mathcal{O}_v/(\varpi)\).
There is no formal Lean code for the lemmas in this section; I am slightly dragging my feet because it would seem more sensible to prove them in the right generality, and we don't have a definition of nonarchimedean local field yet.
LemmaNumberField.isOpenAdicCompletionIntegers#
\(\mathcal{O}_v\) is an open subring of \(K_v\).
Proof
Openness is already in mathlib.
Lean
Formalized as NumberField.isOpenAdicCompletionIntegers.
Sources
Used by 1
\(\mathcal{O}_v\) is also a compact subring of \(K_v\); we proved this in the adele miniproject.
LemmaM2.localFullLevel.isOpen#
\(M_2(\mathcal{O}_v)\) is an open subring of \(M_2(K_v)\).
Proof
Topologically \(M_2(\mathcal{O}_v)\cong \mathcal{O}_v^4\) as a subset of \(K_v^4\) so this follows because a product of compacts is compact and a product of opens is open.
Lean
Formalized as IsDedekindDomain.M2.localFullLevel.isOpen.
Sources
Uses 1
LemmaM2.localFullLevel.isCompact#
\(M_2(\mathcal{O}_v)\) is a compact subring of \(M_2(K_v)\).
Proof
Topologically \(M_2(\mathcal{O}_v)\cong \mathcal{O}_v^4\) as a subset of \(K_v^4\) so this follows because a product of compacts is compact and a product of opens is open.
Lean
Formalized as IsDedekindDomain.M2.localFullLevel.isCompact.
Sources
Uses 1
Recall that there is a projection \(\mathcal{O}_v\to k_v\) where \(k_v\) is the residue field of \(v\), a finite field. This induces a ring homomorphism \(M_2(\mathcal{O}_v)\to M_2(k_v)\) with kernel \(M_2(\varpi\mathcal{O}_v)\), an ideal \(I\) of \(M_2(\mathcal{O}_v)\) isomorphic to \((\varpi\mathcal{O}_v)^4\) and hence also compact and open.
Say \(\Gamma_v\) is a subgroup of \(GL_2(k_v)\). Then \(\Gamma_v\) is finite. Consider it as a submonoid of the multiplicative monoid \(M_2(k_v)\). Its preimage \(U_v\) in \(M_2(\mathcal{O}_v)\) is easily checked to be a submonoid of \(M_2(\mathcal{O}_v)\); furthermore it is a finite union of cosets of \(I\) and is hence compact and open as a submonoid of \(M_2(\mathcal{O}_v)\) and hence of \(M_2(K_v)\).
Say now \(\begin{pmatrix}1&*\\0&1\end{pmatrix}\subseteq\Gamma_v\subseteq\begin{pmatrix}*&*\\0&*\end{pmatrix}\) and let \(U:=U_v\) be its preimage in \(GL_2(\mathcal{O}_v)\), considered as a compact open subgroup of \(GL_2(K_v)\). Choose \(0\not=\alpha\in\mathcal{O}_v\) and define \(g=\begin{pmatrix}\alpha&0\\0&1\end{pmatrix}\in GL_2(K_v)\). Let's do an explicit double coset decomposition in preparation for a calculation with Hecke operators.
LemmabijOn_unipotent_mul_diagU1_U1diagU1#
The double coset space \(UgU\) is the disjoint union of \(g_tU\) as \(t\) ranges through \(\mathcal{O}_v/\alpha\mathcal{O}_v\) and \(g_t:=\begin{pmatrix}\alpha&\tilde{t}\\0&1\end{pmatrix}\), where \(\tilde{t}\) is any lift of \(t\) to \(\mathcal{O}_v\).
Proof
We first manipulate the statement into a statement about finite groups. We have \(UgU=\coprod_t g_tU\iff UgUg^{-1}=\coprod_t g_tUg^{-1}=\coprod_t g_tg^{-1}(gUg^{-1})\). By the second isomorphism theorem this is true if \(U=\coprod_t g_tg^{-1}(gUg^{-1}\cap U)\). So when is an element of \(U\) in \(gUg^{-1}\)? Equivalently, if \(x\in U\), when is \(g^{-1}xg\in U\)? An explicit calculation of matrices shows us that this is true iff \(g=\begin{pmatrix} a&b\\c&d\end{pmatrix}\) with \(\alpha\mid b\). Define \(U^\alpha\) to be this subgroup of \(U\). We have reduced the question to showing that the matrices \(h_t:=\begin{pmatrix}1&\tilde{t}\\0&1\end{pmatrix}\) are a set of left coset representatives for the subgroup \(U^\alpha\) of \(U\).
It thus suffices to show that if \(u=\begin{pmatrix} a&b\\c&d\end{pmatrix}\in U\) then \(u\in h_tU^\alpha\) iff \(b\in\mathcal{O}_v\) reduces mod \(\alpha\) to \(t\in\mathcal{O}_v/\alpha\). We do this by computing \(h_t^{-1}u=\begin{pmatrix} a-\tilde{t}c&b-\tilde{t}d\\c&d\end{pmatrix}\) and observing that its top right hand entry mod \(\alpha\) is zero iff \(b\) mod \(\alpha\) is \(t\).
Lean
Formalized as TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.bijOn_unipotentMulDiagU1.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.