Definitions/Def_ModularCurve_XHDiamondModL.lean

Fix a field K, an integer M and a subgroup H \le (\mathbb{Z}/M)^\times. Here \Gamma_H(M) is the group CohCarrier.GammaH M H, the set of matrices in \Gamma_0(M) whose (1,1)-entry reduces mod M to a unit lying in H, and the field F_K = qExpFunctionFieldC K (CohCarrier.GammaH M H) is the intermediate field of K((q)) = LaurentSeries K generated over K by all quotients \bar p_f/\bar p_g, where f,g run over modular forms of a common integral weight on \Gamma_H(M) (as a subgroup of GL_2(\mathbb{R})), p_f,p_g \in \mathbb{Z}[[q]] are integral q-expansions of f,g at width 1 (i.e. their coefficientwise images in \mathbb{C}[[q]] are the q-expansions), \bar{(\cdot)} denotes the coefficientwise reduction into K((q)) via intSeriesC, and \bar p_g \ne 0.

The module defines a predicate IsDiamondPullbackModL on a group homomorphism \rho from \Gamma_0(M) to the group of K-algebra automorphisms of F_K. It asserts: for every \gamma \in \Gamma_0(M), every weight k \in \mathbb{Z}, all modular forms f,g,f_1,g_1 of weight k on \Gamma_H(M) with integral q-expansions p_f,p_g,p_{f_1},p_{g_1} such that f_1 = f\mid_k\gamma and g_1 = g\mid_k\gamma as functions on the upper half-plane (the slash action of \gamma regarded in SL_2(\mathbb{Z})), and with \bar p_g \neq 0, every element x \in F_K whose underlying Laurent series is \bar p_{f_1}/\bar p_{g_1} satisfies that the Laurent series of \rho(\gamma)(x) is \bar p_f/\bar p_g. Thus \rho(\gamma) carries the reduction of (f\mid\gamma)/(g\mid\gamma) to the reduction of f/g. Non-vanishing is required of \bar p_g only; division by zero in K((q)) is the Lean convention. Nothing is asserted by the definition itself. The accompanying lemma IsDiamondPullbackModL.coe_apply_eq is the same statement in applied form, with the forms, series and element taken as implicit arguments.