The abstract theory
Introduction
The set-up: we have a commutative ring \(R\), the coefficient ring, and all of our spaces which the operators act on will be \(R\)-modules.
We have a group \(G\) acting \(R\)-linearly on an \(R\)-module \(A\).
We have subgroups \(U\) and \(V\) of \(G\). We will be particularly interested in the \(R\)-modules \(A^U\) and \(A^V\) of invariant elements.
Given an element \(g\in G\), then under a certain finiteness hypothesis we will be able to define an \(R\)-linear map \(T_g\) or \([UgV]\) from \(A^V\) to \(A^U\). The finiteness hypothesis is that the double coset \(UgV\) can be written as a finite union of single cosets \(g_iV\).
DefinitionAbstractHeckeOperator.HeckeOperatorToFun#
Assuming \(UgV\) is a finite union of cosets \(g_iV\), we define \([UgV]:A^V\to A^U\) to be the map sending \(a\in A^V\) to \(\sum_i g_ia.\)
LemmaAbstractHeckeOperator.HeckeOperator#
This function is well-defined (that is, independent of the choice of \(g_i\)), has image in \(A^U\) and is \(R\)-linear.
Proof
Well-definedness is because if we change \(g_i\) to \(g'_i:=g_iv\) for some \(v\in V\) then \(g_ia=g_i'a\) because \(a\in A^V\).
The image lands in \(A^U\) because left multiplication by \(u\) fixes \(UgV\) and hence permutes the cosets \(g_iV\).
Finally \(R\)-linearity is because the \(G\)-action is \(R\)-linear.
Lean
Formalized as AbstractHeckeOperator.heckeOperator.
Sources
The group \(G\) is not in general commutative, and hence if \(U=V\) the Hecke operators in this generality do not in general commute as endomorphisms of \(A^U\). Here is a criterion for them to commute.
LemmaAbstractHeckeOperator.comm#
Say \(g,h\in G\) and we have \(UgU=\coprod_i g_iU\) and \(UhU=\coprod_j h_j\) and we have \(g_ih_j=h_jg_i\) for all \(i,j\). Then \([UgU][UhU]=[UhU][UgU]\), that is, the Hecke operators acting on \(A^U\) commute.
Proof
We have \([UgU][UhU]a=\sum_ig_i(\sum_jh_ja)=\sum_{i,j}g_ih_ja\) and \([UhU][UgU]a=\sum_jh_j\sum_ig_ia=\sum_{j,i}h_jg_ia\) and these sums are equal because \(g_ih_j=h_jg_i\).
Lean
Formalized as AbstractHeckeOperator.comm.
Sources
The finiteness hypothesis that the decomposition \(UgV=\coprod_i g_iV\) is into a finite union is necessary for the theory to work. If \(G\) is a topological group then here is a criterion which gives the finiteness hypothesis for free.
LemmaQuotientGroup.mk_image_finite_of_compact_of_open#
If \(U\) and \(V\) are compact subgroups of a topological group \(G\), if \(V\) is also open, and if \(g\in G\), then the double coset space \(UgV\) is a finite union of left cosets \(g_iV\).
Proof
The subset \(UgV\) of \(G\) is a continuous image of the compact set \(U\times V\) and is hence compact, and it is covered by the disjoint left cosets \(g_iV\); this cover must thus be finite.
Lean
Formalized as QuotientGroup.mk_image_finite_of_compact_of_open.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.