claimroutineinferred_dep

Uniform conductor bound gives N ≤ CM²

Bounds conductor at small primes uniformly, giving N≤CM2N\le CM^2
closes the level bound
Claim·§4.8 A uniform bound for the modular level·inside lemModular level is polynomially bounded in M

Statement (paper)

For each fixed prime qq there is an upper ramification cut uqu_q, independent of ss, such that GQquG_{\Q_q}^{u} acts trivially under rℓr_\ell for all u≥uqu\ge u_q. Consequently the Swan conductor of rℓr_\ell at qq is at most 2uq2u_q and its full conductor exponent at qq is bounded by a constant independent of ss. The finitely many fixed primes contribute a constant to NN, and every remaining ramified prime divides MM with exponent at most two, so N≤CM2N\le CM^2, i.e. holds with a=2a=2 after altering the constant CC.

In plain English

For each fixed small prime qq there is an upper ramification cut uqu_q independent of ss beyond which GQquG_{\Q_q}^u acts trivially under rℓr_\ell, so the Swan conductor at qq is at most 2uq2u_q and the conductor exponent at qq is bounded by a constant. Together with the other primes this yields N≤CM2N\le CM^2, i.e. the level bound holds with a=2a=2.

Why it's here

This closes the proof of the level bound: the finitely many fixed primes contribute a constant because the finitely many possible fields F1F_1 from the previous claim give a uniform ramification cut. Every other ramified prime divides MM and is tame with exponent at most two by the large-prime claim, and the level-equals-conductor claim converts these local bounds into the global bound on NN.
Classified routine:
Bookkeeping that combines the earlier claims (level equals Artin conductor, tameness at large primes, uniform ramification cuts) with the standard bound of the Swan conductor by the upper ramification break. It also uses the finiteness of local extensions of bounded degree (Krasner's lemma).

Uses

claimLevel exponents equal Artin conductorsclaimLarge primes in T are tameclaimUniform ramification cut for betaclaimWild inertia acts trivially over F_1

Used by

Nothing in the paper

Sources

PaperOpen
Section
§4.8 A uniform bound for the modular level
Page
—
Label
—
Line
sections/04-height.tex:1122
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-1
  • info
    inferred_dep
    outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-2
  • info
    inferred_dep
    outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-3
  • info
    inferred_dep
    outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-4