Definitions/Def_ModularCurve_Eisenstein.lean

Four predicates (def … : Prop) in namespace ModularCurve that instantiate the generic Eisenstein/Hecke calculus of the project's HeckeGalois_EichlerShimura layer at the concrete carriers JZero p, eisensteinIdeal p, heckePic0Bar and cuspidalClass p. Each takes p : ℕ with only [NeZero p] (primality and size conditions are left to consuming theorems), and the first, second and fourth take an explicit binder inst : Module HeckeAlg (JZero p), installed locally by letI, since no ambient Hecke-module structure on JZero p is assumed at this point. EisensteinQuotientInvariantsFiniteAt p inst is the project's generic predicate EisensteinQuotientInvariantsFinite applied with group G the automorphism group \bar{\mathbb Q}\simeq_{\mathbb Q}\bar{\mathbb Q}, module JZero p and ideal eisensteinIdeal p; its intended reading is finiteness of the Galois invariants of the Eisenstein quotient, but what the Prop asserts is exactly the unfolding of that project notion, and no commutation of the Hecke action with G is required by the binders. SpecializationSlot p q inst is the project's SpecializationExists at K=\mathbb Q, L=\bar{\mathbb Q}, the pair (p,q) and the module JZero p. HeckeKillsCuspidalClass p ℓ hα hβ hFI hfin hN carries, in order, the inputs demanded by heckePic0Bar: integrality hypotheses HeckeAlphaBarIntegral/HeckeBetaBarIntegral for the two Hecke correspondence maps at level p\ell, a HasPrincipalDivisors instance for modularFunctionFieldBar (p * ℓ), a fundamental identity FundamentalIdentityAlong, finiteness FiniteAlong and a norm formula NormFormulaAlong; its conclusion is the pointwise equation \mathrm{heckePic0Bar}(\text{cuspidalClass } p) - (1+\ell)\cdot\text{cuspidalClass } p = 0, i.e. T_\ell acts on the cuspidal class by 1+\ell, written as a subtraction rather than as an operator T_\ell-(1+\ell). EisensteinKernelKillsCuspidalClass p inst says every t in eisensteinKernel (JZero p) (eisensteinIdeal p) satisfies t\cdot\text{cuspidalClass } p = 0. None of the four is a theorem here: the module proves nothing about X_0(N) and states nothing about the order of the cuspidal class.