Prime divisors of a residual kernel-field discriminant divide Np

Proved

HorizontalPadicL.residualKernel_discr_prime_dvd_level_mul_p

by davidloeffler · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

discriminantsgalois-representationsmodular-formsnumber-theoryramification

Let $f$ be an MTT eigenform of positive level $N$ and weight $k\geq 2$ , let $p$ be prime, and let $D$ be residual Galois-representation data for $f$ at a chosen $p$ -adic embedding. If a rational prime $\ell$ divides the discriminant of the finite Galois kernel field recorded by $D$ , then $\ell$ divides $Np$ . Equivalently, the kernel field is discriminantly unramified away from the modular level and the residue characteristic.

Preamble

import Definitions.Def_KN_EigenformResidualGaloisRepresentationV2
import Mathlib.NumberTheory.NumberField.Discriminant.Different

set_option autoImplicit false
noncomputable section

namespace HorizontalPadicL

Formal statement

/-- Every rational prime dividing the discriminant of the kernel field of an
eigenform's residual Galois representation divides the product of the modular
level and the residue characteristic. -/
theorem residualKernel_discr_prime_dvd_level_mul_p
    {N k p : ℕ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k)
    {ι : MTT.Qbar →+* ℂ}
    (f : MTT.Eigenform N k ι) (ιp : MTT.Qbar →+* ℂ_[p])
    (D : EigenformResidualGaloisRepresentationData hN hk f ιp) :
    letI : Field D.kernelField := D.kernelField_field
    letI : NumberField D.kernelField := D.kernelField_numberField
    ∀ {l : ℕ}, l.Prime →
      (l : ℤ) ∣ NumberField.discr D.kernelField → l ∣ N * p := by sorry

end HorizontalPadicL

Source

The discriminant criterion for unramified rational primes, `NumberField.not_dvd_discr_iff_forall_liesOver`, together with the equality between the order of the inertia group and the ramification index.

View graph