The goal

The goal of this project is to get sorry-free definitions of Hecke operators acting on spaces of automorphic forms. These Hecke operators generate Hecke algebras, which are the rings called \(T\) in the modularity lifting theorems, or \(R=T\) theorems, crucially introduced by Wiles in order to prove FLT.

The theory comes in two parts; the “abstract” theory, which is pure algebra, and the “concrete” theory where we apply the abstract constructions to produce endomorphisms of spaces of automorphic forms. The abstract theory is short (and completely formalized); the concrete theory still needs some work because to apply the theory to the adelic groups we care about we need to develop some more API around the theory of restricted products, and of compact open subgroups of matrix groups.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.