Extensions of bounded degree unramified outside a finite set

Let K be a number field and S a finite set of finite places of K. This file proves Hermite's finiteness theorem (often called the Hermite–Minkowski theorem) in the form used for Galois cohomology unramified outside S: inside any field A containing K, there are only finitely many extensions L / K of degree at most d whose ramified places all lie in S. Finiteness theorems for Galois cohomology groups unramified outside S, such as the finiteness of Selmer groups over number fields, reduce to this statement.

The proof bounds the discriminant and applies Hermite's theorem NumberField.finite_of_discr_bdd. The bound comes from the different. At a prime P of 𝓞 L with ramification index e over K, the wild bound says the different exponent is at most e - 1 + v_P(e), and e ≤ [L : K]. Now e divides [L : K]!, and v_P(𝔭) = e for the prime 𝔭 of K below P. So the different divides [L : K]! · ∏ 𝔭, the product over the ramified primes 𝔭 of K. Taking norms,

|d_L| ∣ (N([L : K]! · ∏ 𝔭) · |d_K|) ^ [L : K].

The factor [L : K]! is crude, but this bound depends only on [L : K] and the ramified primes, which is all the finiteness argument needs.

Main results

• TauCeti.NumberField.differentIdeal_dvd_map_span_factorial_mul_prod_ramifiedSupport: the different of L / K divides [L : K]! times the product of the ramified primes of K.
• natAbs_discr_dvd_absNorm_factorial_mul_prod_ramifiedSupport_mul_natAbs_discr_pow (in TauCeti.NumberField): the resulting divisibility of the absolute discriminant of L.
• TauCeti.NumberField.finite_of_finrank_le_of_ramifiedSupport_subset: there are finitely many extensions of K in A of degree at most d and ramified only at places in S.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, §2.

theorem TauCeti.NumberField.differentIdeal_dvd_map_span_factorial_mul_prod_ramifiedSupport {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ∣ Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (Ideal.span {↑(Module.finrank K L).factorial} * ∏ v ∈ ramifiedSupport K L, v.asIdeal)

The different divides [L : K]! times the product of the ramified primes. The different of L / K divides the extension to 𝓞 L of [L : K]! · ∏ 𝔭, where 𝔭 runs over the primes of 𝓞 K ramified in L.

theorem TauCeti.NumberField.natAbs_discr_dvd_absNorm_factorial_mul_prod_ramifiedSupport_mul_natAbs_discr_pow {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : (NumberField.discr L).natAbs ∣ (Ideal.absNorm (Ideal.span {↑(Module.finrank K L).factorial} * ∏ v ∈ ramifiedSupport K L, v.asIdeal) * (NumberField.discr K).natAbs) ^ Module.finrank K L

A bound on the discriminant from the ramified primes. The absolute discriminant of L divides (N([L : K]! · ∏ 𝔭) · |d_K|) ^ [L : K], the product over the primes 𝔭 of K ramified in L.

theorem TauCeti.NumberField.finite_of_finrank_le_of_ramifiedSupport_subset {K : Type u_1} [Field K] [NumberField K] (A : Type u_3) [Field A] [Algebra K A] (d : ℕ) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : {L : { F : IntermediateField K A // FiniteDimensional K ↥F } | Module.finrank K ↥↑L ≤ d ∧ ramifiedSupport K ↥↑L ⊆ S}.Finite

Hermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set. Inside a field A containing the number field K, only finitely many finite extensions L / K have degree at most d and are ramified only at places in the finite set S.