claimroutineinferred_dep

Large primes in T are tame

Shows rℓr_\ell is tame at large primes of TT, exponent ≤2\le2
bounds conductors at large primes
Claim·§4.8 A uniform bound for the modular level·inside lemModular level is polynomially bounded in M

Statement (paper)

Let q∈Tq\in T be larger than a fixed constant that includes all primes in SS, the primes 2,32,3, and the uniform upper bound for [L:Q][L:\Q]. Then rℓr_\ell (and RℓR_\ell) is tame at qq, and hence the conductor exponent of the newform at qq is at most two.

In plain English

For a prime q∈Tq\in T larger than a fixed constant (exceeding all primes in SS, the primes 2 and 3, and the uniform bound on [L:Q][L:\Q]), the representation rℓr_\ell (and RℓR_\ell) is tame at qq. Hence the newform's conductor exponent at qq is at most two.

Why it's here

This handles the large primes of TT in the level bound: tameness caps the local conductor exponent at two, so each such prime contributes a bounded factor. The ingredients are that L/QL/\Q is unramified outside TT with uniformly bounded degree (hei-hom-field), and that the correcting cochain β\beta and its character χ\chi are tame at odd primes with bounded local conductor (hei-sign-splitting). Together with the small-prime analysis in the later claim, this gives the polynomial bound on NN.
Classified routine:
Follows directly from the earlier lemmas hei-hom-field (bounded-degree field L unramified outside T) and hei-sign-splitting (tame β, χ at odd primes). It then applies the standard fact that a tamely ramified ℓ-adic representation at q has conductor exponent at most its dimension, here at most two.

Uses

lemSign-splitting cochain with square-root characterlemBounded field for all geometric homomorphisms

Used by

claimUniform conductor bound gives N ≤ CM²

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Large primes in T are tame with exponent at most two" rests on hei:sign-splitting
  • info
    inferred_dep
    outline: "Large primes in T are tame with exponent at most two" rests on hei:hom-field