Definitions/Def_ModularCurve_HeckeNamedInputs.lean

Throughout, L is a field equipped with a \mathbb{Q}-algebra structure, and for a nonzero level N the relevant curve is presented by the intermediate field L-generated inside \mathrm{LaurentSeries}(L) by the coefficientwise image of \mathrm{modularFunctionFieldFull}(N), the subfield of \mathrm{LaurentSeries}(\mathbb{Q}) generated by the q-expansions j(q^{d}) for d \mid N. Two degeneracy embeddings into level N\ell are available: heckeAlphaBar, the inclusion of the level-N field into the level-N\ell field, and heckeBetaBar, induced by the substitution q \mapsto q^{\ell} (qExpand L ℓ); towerSubstBar L N ℓ h is the latter followed by the inclusion into a larger level M with N\ell \mid M. Divisors are transported by Divisor.pullbackAlong and Divisor.pushforwardAlong along such an algebra map together with a witness that it is integral, and heckeDivBar is the induced correspondence on divisors, pullback along \beta followed by pushforward along \alpha.

HeckeDiagonalIdentity L N p is the proposition, universally quantified over two HasPrincipalDivisors instances (at levels Np and Np^{2}), over integrality witnesses for \alpha,\beta at (N,p) and at (Np,p), over an L-algebra automorphism \sigma of the level-Np field with heckeBetaBar L N p followed by \sigma equal to heckeAlphaBar L N p, over integrality of \sigma, and over a divisor D on the level-Np field, that the pullback along \beta_{N,p} of the pushforward along \alpha_{N,p} of D equals heckeDivBar at the level pair (Np,p) applied to D plus the pushforward of D along \sigma. Classically this is the one-prime double-coset decomposition, the extra term being the graph of the Atkin–Lehner involution.

HeckeBetaExchangeAt L N ℓ ℓ' M hM, for M = N\ell\ell', asserts under the corresponding instances, integrality witnesses for \beta_{N,\ell}, \beta_{N,\ell'} and the two substitution maps to level M, and for every divisor D on the level-N\ell' field, that pullback along \beta_{N,\ell} of pushforward along \beta_{N,\ell'} of D equals the pushforward along towerSubstBar L (N * ℓ) ℓ' of the pullback along towerSubstBar L (N * ℓ') ℓ of D. The helper dvd_of_eq_roof_beta supplies the two divisibilities N\ell\ell' \mid M and N\ell'\ell \mid M needed to name those substitution maps.