Definitions/Def_ModularCurve_LevelOneProlongationPairRegularity.lean

Fix a prime q, a valuation subring A of \overline{\mathbb Q}, a field k of characteristic q with a ring map \mathrm{red}\colon A\to k, modular polynomial data for q with its Kronecker congruence, the two Hecke integrality hypotheses at level one, a place specialisation P over these data, and a level-one prolongation pair R for P; write \rho_1,\rho_2 for the two residue maps R.\mathrm{residue}_1,R.\mathrm{residue}_2, which send the valuation rings R.R₁.integers, R.R₂.integers inside the geometric level-q modular function field modularFunctionFieldBar (1 * q) into modularFunctionFieldC k 1, and \varphi for frobOnPlacesGeomLevel k 1 data hKr acting on the places of modularFunctionFieldC k 1 over k.

For a finite set S_0\subseteq k, the predicate RegularityLaw S₀ is the conjunction of two clauses, both quantified over every f in the level-q field lying in both valuation rings. First: for every place v with \varphi(\varphi v)=v and v\neq P.\mathrm{redFst} of the cusp \infty at level q, if \operatorname{ord}_W f\ge 0 for every place W of the level-q field with P.\mathrm{redFst}\,W=v, then \operatorname{ord}_v(\rho_1 f)\ge 0 whenever \rho_1 f\neq 0, and \operatorname{ord}_{\varphi v}(\rho_2 f)\ge 0 whenever \rho_2 f\neq 0. Second: for every a\in S_0 with a^{q^2}=a, if \operatorname{ord}_W f\ge 0 for every W with P.\mathrm{redFst}\,W equal to the place j=a (the first component of frobNodePair q a), then there is a single c\in k such that \rho_1 f has value c at the place j=a and \rho_2 f has value c at the place j=a^q. No non-vanishing of c is demanded, in contrast with LevelOneProlongationPair.NodeValueLaw, where c\neq 0 is required and the admissible j-invariants are those in ssJSet q k. The module asserts nothing; it only names this proposition.