The goal

At the time of writing, mathlib still does not have a proof that the space of classical modular forms of a fixed weight, level and character is finite-dimensional. The main result in this miniproject is to prove that certain spaces of quaternionic modular forms are finite-dimensional. We need finiteness results like this in order to control the Hecke algebras which act on these spaces; these Hecke algebras are the “\(T\)”s which are isomorphic to the “\(R\)”s in the \(R=T\) theorem which is the big first target for the FLT project.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.