Definitions/Def_MDivRepresents.lean

Standing context: a prime q, a valuation subring A of \overline{\mathbb Q}, a level N\neq 0, a field k of characteristic q with a ring homomorphism red : A \to k, and data data, hKr, hα, hβ describing a modular polynomial with its Kronecker congruence and the integrality of the two Hecke degeneracy maps. Two abbreviations name elements of the geometric level-Nq function field modularFunctionFieldBar (N * q): jNFun is the q-expansion j(Nz) and jNQFun is j(Nqz), each placed in that field by base change of coefficients to \overline{\mathbb Q}; alongside them sit ProlongationTuple.jFun (j) and ProlongationTuple.jQFun (j(qz)). evalBar N q c H evaluates a polynomial H in the three variables indexed by Option (Fin 2) with coefficients in A at an assignment c of those variables by elements of the level-Nq field, the coefficients being mapped along A \hookrightarrow \overline{\mathbb Q} \to F. The predicates IsFstTriple v c z y₁ y₂ and IsSndTriple v c z y₁ y₂, for a place v of the level-N function field over k and c \in k, each assert a disjunction of two normalisations: for IsFstTriple either (z,y_1,y_2)=(j,\,j_N,\,j_{Nq}) together with \mathrm{ord}_v(\mathtt{jGeomGen}\,k\,N - c)=1, or (z,y_1,y_2)=(j_N,\,j,\,j_{Nq}) together with \mathrm{ord}_v(\mathtt{jNGeomGen}\,k\,N - c)=1; for IsSndTriple the triples are (j_q,\,j_{Nq},\,j) and (j_{Nq},\,j_q,\,j) with the same two uniformiser conditions. Thus the relevant generator downstairs, shifted by c, is required to be a uniformiser at v.

MDivRepresents is a predicate on: a place specialisation P; tuples Q_1 : \mathrm{Fin}\,d_1 \to places of the level-Nq geometric field, Q_2 : \mathrm{Fin}\,d_2 \to such places, and a second pair Q_1', Q_2' of the same shapes; a natural number m'; a family h of (d_1+d_2)m'+1 elements of that field; and incidence data D of type IncidenceSystem.Data (d₁ + d₂) 2 m' A. It is the conjunction of two clauses. First, for every index i of \mathrm{Fin}(d_1+d_2) there exist z, y_1, y_2 in the level-Nq field and \tau \in A such that, splitting i through \mathrm{Fin}\,d_1 \oplus \mathrm{Fin}\,d_2: the triple satisfies IsFstTriple at P.reduceFst (Q₁ i₁) with c = red(D.u₀\,i) in the left case, and IsSndTriple at P.reduceSnd (Q₂ i₂) in the right case; both polynomials G_{i,0}, G_{i,1} of D vanish at (z,y_1,y_2) and the variable some 1 does not occur in G_{i,0}; at the i-th place of the concatenation of Q_1 and Q_2 one has \mathrm{ord}(z - D.u₀\,i) > 0 and \mathrm{ord}(y_j - D.w₀\,i\,j\,0) > 0 for j = 0,1, while at the i-th place of the concatenation of Q_1' and Q_2' one has \mathrm{ord}(z - \tau) > 0; for every kk in Option (Fin ((d₁ + d₂) * m')) the identity p_{kk,i}(z,y_1,y_2) = c_{kk}\,(z - D.u₀\,i)^{m'}(z-\tau)\,s_{kk,i}(z,y_1,y_2) holds, with c_{kk} = 1 for kk = \mathrm{none} and c_{kk} = h(k.\mathrm{succ}) for kk = \mathrm{some}\,k; the \mathrm{none} component is pinned exactly, D.p\,\mathrm{none}\,i = (X_{\mathrm{none}} - u^0_i)^{m'}(X_{\mathrm{none}} - \tau), D.s\,\mathrm{none}\,i = 1 and D.\sigma_0\,\mathrm{none}\,i = the jet supported at index 0 with value 1; and finally the reductions red(D.sVal\,D.centre\,kk\,i) and red(D.dG\,D.centre\,i\,j) are all non-zero, i.e. the values of the s_{kk,i} and the partial derivatives \partial_{y_j} G_{i,j} at the centre of D are units of A. Second, for every variable v of the incidence system IncidenceSystem.Var (d₁ + d₂) 2 m', the value of the system polynomial D.\mathrm{system}\,v at D.\mathrm{centre} lies in the maximal ideal of A, so that the centre is a root of the system modulo \mathfrak m_A. The definition asserts nothing by itself; it records the compatibility between analytic data on the level-Nq curve and the purely polynomial incidence data over A.