Definitions/Def_ModularCurve_LevelOneGlueData.lean

Fix a prime q, a valuation subring A of \overline{\mathbb Q}, a field k of characteristic q with a ring homomorphism \mathrm{red}\colon A\to k, modular polynomial data data for q with its Kronecker congruence hKr, integrality hypotheses h\alpha,h\beta for the two degeneracy maps between levels 1 and 1\cdot q, and a place specialisation P (the project's structure PlaceSpecialization at level N=1), whose component P.sp sends places of the level-one modular function field over \overline{\mathbb Q} to places of modularFunctionFieldC k 1. For a place W of the level-(1\cdot q) function field over \overline{\mathbb Q}, redFst W is P.\mathrm{sp} applied to the restriction of W along heckeAlphaBar (the inclusion of the level-one field), and redSnd W is P.\mathrm{sp} applied to the restriction along heckeBetaBar (the map induced by the substitution q\mapsto q^{\,\ell} on Laurent expansions). Writing \varphi for frobOnPlacesGeomLevel k 1 data hKr, the map on places induced by the q-power Frobenius endomorphism of modularFunctionFieldC k 1, the predicate IsStrictTypeOne W asserts \varphi(\mathrm{redFst}\,W)=\mathrm{redSnd}\,W and \varphi^2(\mathrm{redFst}\,W)\ne \mathrm{redFst}\,W, and IsStrictTypeTwo W asserts \mathrm{redFst}\,W=\varphi(\mathrm{redSnd}\,W) and \varphi^2(\mathrm{redSnd}\,W)\ne\mathrm{redSnd}\,W. A divisor is a good divisor when every place in its support satisfies one of these two conditions; fstPart and sndPart are the restrictions of a divisor (as a finitely supported function) to the places of strict type one, resp. two, and branchDegrees records the pair of their degrees.

For a finite set S of pairs of places of modularFunctionFieldC k 1, levelOneGlueData S D is the element of the project's type GluingData given by the triple consisting of the pushforward of fstPart D along redFst, the pushforward of sndPart D along redSnd, and 0 in the third (node-unit) component. Finally, IsLevelOneGluedSpecialization S sp is a specification on an additive map sp from the inertia invariants inertiaInvariants A (1 * q) in J_0(1\cdot q) to GluedPic0 k (modularFunctionFieldC k 1) S: for every degree-zero divisor D whose class lies in those inertia invariants and every admissible gluing datum x, if D is good and x equals levelOneGlueData S D, then sp of the class of D equals GluedPic0.mk S x. Nothing is required of sp on classes outside this range of data, so this is a constraint on sp rather than a construction of it.