Definitions/Def_ModularCurve_ShimuraSubgroup.lean

Two predicates on additive subgroups of the Jacobian JZero N, the degree-zero divisor class group of the base change to \overline{\mathbb{Q}} of the modular function field of level N, carrying the Galois action induced coefficientwise on Laurent series. First, IsMuTypeJZeroSubgroup N S is a structure with two fields: galoisStable, saying that \sigma \cdot x \in S for every \mathbb{Q}-algebra automorphism \sigma of \overline{\mathbb{Q}} and every x \in S; and galoisActsCyclotomic, saying that for every natural number n, every x \in S with n x = 0, every \sigma and every natural number k such that \sigma \zeta = \zeta^{k} for all \zeta \in \overline{\mathbb{Q}} with \zeta^{n} = 1, one has \sigma \cdot x = k x. Thus S is Galois-stable and, on each n-torsion layer, Galois acts through the mod-n cyclotomic character; the clause is imposed for all n, not only prime n. (For n = 0 the hypothesis on \sigma and k forces k = 1 and \sigma = \mathrm{id}, so nothing is required there.)

Second, for a prime p, IsShimuraSubgroup p S is a structure with three fields: S is of \mu-type in the above sense; for every prime \ell and every x \in S, \bar{T}_\ell x = e_N(\ell)\, x where e_N(\ell) is the Eisenstein system, equal to 1 if \ell \mid p and to 1 + \ell otherwise; and \operatorname{card} S = (p-1)/\gcd(p-1,12), the Eisenstein numerator. Since that numerator is at least 1, the cardinality clause forces S to be finite of exactly that order. Two accompanying lemmas record that the trivial subgroup is of \mu-type, and that it is a Shimura subgroup whenever the Eisenstein numerator equals 1, as happens for p = 13.