Definitions/Def_ModularCurve_HeckeInputsAll.lean

This module defines a single predicate, ModularCurve.HeckeInputsAll N (for N with NeZero N), asserting that for every prime \ell — with the instance \ell\neq 0 installed from primality — the project's predicate HeckeInputsAlong (AlgebraicClosure ℚ) N ℓ holds. The latter is a (dependent) conjunction of the data needed to realise the Hecke correspondence as an endomorphism of \mathrm{Pic}^0 of the base-changed modular function field. Concretely, write \bar F_M for laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull M), the \overline{\mathbb Q}-subfield of \overline{\mathbb Q}-Laurent series generated coefficientwise by the field \mathbb Q(q^{d}\text{-expansions } j(d\tau) : d\mid M); its degree-zero divisor class group is JZero M. The two maps are \alpha= heckeAlphaBar, the inclusion \bar F_N\subseteq\bar F_{N\ell} coming from N\mid N\ell, and \beta= heckeBetaBar, induced by the substitution q\mapsto q^{\ell} on Laurent series (i.e. f(\tau)\mapsto f(\ell\tau)). The conjuncts are: integrality of \bar F_{N\ell} over \bar F_N along \alpha and along \beta; the instance HasPrincipalDivisors for \bar F_{N\ell}, i.e. each nonzero function admits a finitely supported divisor of its orders at all places, of degree 0; module-finiteness along \alpha; the fundamental identity along \beta, \sum_{w\mid v} e_w\deg w=[\bar F_{N\ell}:\bar F_N]\deg v for every place v; and the pushforward norm formula along \alpha, expressing \alpha_*(\mathrm{div}\,g) at each place v as v(\mathrm{N}_{\bar F_N}g). These are exactly the hypotheses consumed by heckePic0Bar, which builds T_\ell=\alpha_*\circ\beta^{*} on JZero N. Nothing is asserted here beyond the definition; HeckeInputsAll is a hypothesis to be supplied.