A finite, coefficient-free cover of the finite prime ideals that can ramify in a subextension of a number field. The cover is constructed from rational primes dividing the absolute discriminant, and its size is bounded by the field degree times their number.

noncomputable def CCDN.rationalPrimeIdealFiber (K : Type u_1) [Field K] [NumberField K] (p : ℕ) : Finset (Ideal (NumberField.RingOfIntegers K))

The finite set of prime ideals of 𝓞 K lying over the rational prime ideal (p).

Equations

• CCDN.rationalPrimeIdealFiber K p = ⋯.toFinset

noncomputable def CCDN.discriminantPrimeIdealCover (K : Type u_1) [Field K] [NumberField K] : Finset (Ideal (NumberField.RingOfIntegers K))

The finite set of prime ideals of 𝓞 K lying over rational primes dividing the absolute discriminant of K; it contains every nonzero prime that ramifies in some subextension.

Equations

• CCDN.discriminantPrimeIdealCover K = (NumberField.discr K).natAbs.primeFactors.biUnion (CCDN.rationalPrimeIdealFiber K)

theorem CCDN.discriminantPrimeIdealCover_card_le (K : Type u_1) [Field K] [NumberField K] : (discriminantPrimeIdealCover K).card ≤ Module.finrank ℚ K * (NumberField.discr K).natAbs.primeFactors.card

The discriminant prime-ideal cover has at most [K : ℚ] times the number of prime factors of the absolute discriminant.

theorem CCDN.absolute_discriminant_power_le (K : Type u_1) [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra F K] : (NumberField.discr F).natAbs ^ Module.finrank F K ≤ (NumberField.discr K).natAbs

Discriminant descent in its exact extension-degree form.

theorem CCDN.quadratic_absolute_discriminant_square_le (K : Type u_1) [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra F K] (hd : Module.finrank F K = 2) : (NumberField.discr F).natAbs ^ 2 ≤ (NumberField.discr K).natAbs

For a quadratic extension K / F of number fields, |discr F| ^ 2 ≤ |discr K|.

theorem CCDN.mem_discriminantPrimeIdealCover_of_ramification_two (K : Type u_1) [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra F K] (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] (hQ : Q ≠ ⊥) (he : Q.ramificationIdx (NumberField.RingOfIntegers F) = 2) : Q ∈ discriminantPrimeIdealCover K

Relative ramification index two forces the prime into the finite discriminant cover.