The inertia subgroups generate the Galois group of a number field

Let K be a number field that is Galois over ℚ, with Galois group G acting on the ring of integers 𝓞 K. Each maximal ideal P of 𝓞 K carries an inertia subgroup P.inertia G, the elements of G acting trivially on 𝓞 K ⧸ P, and its cardinality is the ramification index of P over ℤ (Ideal.card_inertia_eq_ramificationIdx, in TauCeti/NumberTheory/RamificationInertia/Galois.lean). This file proves that these subgroups generate all of G:

⨆ P : MaximalSpectrum (𝓞 K), P.asIdeal.inertia G = ⊤.

The engine is a dictionary between ramification in an intermediate field and containment of inertia subgroups. For a subgroup H with fixed field F and a prime P of 𝓞 K, the prime of 𝓞 F below P is unramified over ℤ exactly when P.inertia G ≤ H: multiplicativity of ramification in the tower ℤ ⊆ 𝓞 F ⊆ 𝓞 K writes e(P / ℤ) as e(𝔮 / ℤ) * e(P / 𝓞 F), and the two absolute indices are the cardinalities of P.inertia G and of P.inertia H, which is P.inertia G ⊓ H. Quantifying over the primes above a rational prime p turns this into a test for ramification of p in F, and when the Galois group is commutative all those primes share an inertia subgroup, so a single prime upstairs suffices.

Generation is then Minkowski's theorem. If H contains every inertia subgroup, the dictionary makes its fixed field F unramified over ℚ at every finite prime, and Minkowski's bound on the discriminant (NumberField.exists_not_isUnramifiedIn) leaves F = ℚ, that is H = ⊤.

This is the missing input flagged as a TODO of Mathlib/RingTheory/Polynomial/Morse.lean, whose Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top takes generation by inertia subgroups as a hypothesis.

The second half of the file draws the consequence that genus theory needs. If M is abelian over ℚ and unramified at all finite places over the fixed field F of a subgroup H, then the inertia subgroup of a prime of 𝓞 M meets Gal(M/F) trivially, so every element of it is killed by the index of H. Generation by inertia promotes this to all of Gal(M/ℚ), whose exponent therefore divides H.index = [F : ℚ]. Taking F quadratic is the classical first step towards the genus field being multiquadratic; the passage from exponent 2 to a compositum of quadratic fields is Kummer theory over ℚ and is not formalised here.

Main results

• NumberField.ramificationIdx_under_eq_one_iff_inertia_le: unramifiedness of the intermediate prime below P is containment of the inertia subgroup of P.
• NumberField.notMem_ramifiedPrimes_iff_forall_inertia_le: the same dictionary for a rational prime, quantified over the primes of 𝓞 K above it.
• NumberField.notMem_ramifiedPrimes_iff_inertia_le: for a commutative Galois group, one prime upstairs suffices.
• NumberField.eq_top_of_forall_inertia_le: a subgroup of G containing every inertia subgroup is ⊤.
• NumberField.iSup_inertia_eq_top: the packaged generation statement.
• NumberField.disjoint_inertia_of_ramificationIdx_eq_one: if P is unramified over the fixed field of H, then the inertia subgroup at P meets H trivially.
• NumberField.pow_index_eq_one_of_isUnramifiedIn: if G is abelian and K is unramified over the fixed field F of H at every prime of 𝓞 F, then the exponent of G divides H.index, which is Module.finrank ℚ F by IsGaloisGroup.index_eq_finrank (in TauCeti/FieldTheory/Galois/IsGaloisGroup.lean).
• NumberField.aut_exponent_dvd_finrank_of_isUnramifiedIn: the resulting degree bound for the automorphism group of an abelian number-field extension and an arbitrary intermediate field.
• NumberField.ramifiedPrimes_iSup: a compositum of intermediate fields of a number field ramifies exactly at the primes ramifying in one of them.
• TauCeti.NumberField.exists_mem_inertia_apply_eq_neg: if a prime p ramifies in the quadratic field generated by a square root x of a rational number, then every prime above p has an inertia element negating x.

References

Generation of a Galois group by inertia subgroups is Section 4.4 of [J. P. Serre, Topics in Galois Theory][serre-galois]; the genus-theoretic consequence is the standard proof that the genus field is multiquadratic, as in D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: from Euler to Eisenstein, §2.2.

theorem NumberField.finrank_eq_one_of_forall_ramificationIdx_eq_one {F : Type u_1} [Field F] [NumberField F] (h : ∀ (q : Ideal (RingOfIntegers F)), q.IsPrime → q ≠ ⊥ → q.ramificationIdx ℤ = 1) : Module.finrank ℚ F = 1

A number field unramified at every finite prime is ℚ. If every nonzero prime of 𝓞 F is unramified over ℤ, then Module.finrank ℚ F = 1. This is Minkowski's bound on the discriminant, in the form NumberField.exists_not_isUnramifiedIn.

theorem NumberField.ramificationIdx_under_eq_one_iff_inertia_le {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] {F : Type u_3} [Field F] [Algebra F K] (H : Subgroup G) [IsGaloisGroup (↥H) F K] (P : Ideal (RingOfIntegers K)) (hP : P.IsPrime) : (Ideal.under (RingOfIntegers F) P).ramificationIdx ℤ = 1 ↔ Ideal.inertia G P ≤ H

Unramifiedness in an intermediate field is containment of inertia. Let H be a subgroup of G with fixed field F, and let P be a prime of 𝓞 K. The prime of 𝓞 F below P is unramified over ℤ exactly when the inertia subgroup of P is contained in H.

Both directions come from one computation: multiplicativity of ramification in the tower ℤ ⊆ 𝓞 F ⊆ 𝓞 K writes e(P / ℤ) as e(𝔮 / ℤ) * e(P / 𝓞 F), while Ideal.card_inertia_eq_ramificationIdx reads the two absolute indices as the cardinalities of P.inertia G and of P.inertia H = P.inertia G ⊓ H. So e(𝔮 / ℤ) = 1 says exactly that the intersection is everything.

NumberField.disjoint_inertia_of_ramificationIdx_eq_one is the complementary statement, about P being unramified over 𝓞 F rather than 𝔮 over ℤ.

theorem NumberField.notMem_ramifiedPrimes_iff_forall_inertia_le {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] {F : Type u_3} [Field F] [NumberField F] [Algebra F K] (H : Subgroup G) [IsGaloisGroup (↥H) F K] {p : ℕ} (hp : Nat.Prime p) : p ∉ ramifiedPrimes F ↔ ∀ (P : Ideal (RingOfIntegers K)), P.IsPrime → P.LiesOver (Ideal.span {↑p}) → Ideal.inertia G P ≤ H

Ramification of a rational prime in an intermediate field, read off the inertia subgroups. Let H be a subgroup of G with fixed field F. A rational prime p is unramified in F exactly when the inertia subgroup of every prime of 𝓞 K above p is contained in H.

Every prime of 𝓞 F above p is the prime below some prime of 𝓞 K above p, so this is NumberField.ramificationIdx_under_eq_one_iff_inertia_le quantified over the primes upstairs.

theorem NumberField.notMem_ramifiedPrimes_iff_inertia_le {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] {F : Type u_3} [Field F] [NumberField F] [Algebra F K] [IsMulCommutative G] (H : Subgroup G) [IsGaloisGroup (↥H) F K] {p : ℕ} (hp : Nat.Prime p) (P : Ideal (RingOfIntegers K)) (hP : P.IsPrime) (hPp : P.LiesOver (Ideal.span {↑p})) : p ∉ ramifiedPrimes F ↔ Ideal.inertia G P ≤ H

Ramification of a rational prime in an intermediate field, tested at one prime upstairs. Let H be a subgroup of the abelian Galois group G with fixed field F, and let P be a prime of 𝓞 K above the rational prime p. Then p is unramified in F exactly when the inertia subgroup of P is contained in H.

Only one prime P above p has to be inspected: a commutative Galois group acts transitively on the primes above p and translation conjugates inertia subgroups, so they all share one inertia subgroup (Ideal.inertia_eq_of_liesOver).

theorem NumberField.eq_top_of_forall_inertia_le {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] {H : Subgroup G} (h : ∀ (P : Ideal (RingOfIntegers K)), P.IsMaximal → Ideal.inertia G P ≤ H) : H = ⊤

A subgroup containing every inertia subgroup is everything. Let K be a number field Galois over ℚ with Galois group G. If a subgroup H of G contains the inertia subgroup of every maximal ideal of 𝓞 K, then H = ⊤.

The fixed field F of H inherits no ramification: for a prime P of 𝓞 K the inertia subgroups of P in H and in G coincide, so the ramification indices e(P / ℤ) and e(P / 𝓞 F) agree and the intermediate index e(𝔮 / ℤ) is 1. By Minkowski's theorem a number field unramified over ℚ is ℚ, so F = ℚ.

@[simp]

theorem NumberField.iSup_inertia_eq_top {K : Type u_1} [Field K] [NumberField K] (G : Type u_2) [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] : ⨆ (P : MaximalSpectrum (RingOfIntegers K)), Ideal.inertia G P.asIdeal = ⊤

The inertia subgroups generate the Galois group. For a number field K Galois over ℚ with Galois group G, the supremum of the inertia subgroups of the maximal ideals of 𝓞 K is ⊤.

theorem NumberField.disjoint_inertia_of_ramificationIdx_eq_one {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] {F : Type u_3} [Field F] [Algebra F K] (H : Subgroup G) [IsGaloisGroup (↥H) F K] (P : Ideal (RingOfIntegers K)) (hP : P.IsPrime) (hunr : P.ramificationIdx (RingOfIntegers F) = 1) : Disjoint (Ideal.inertia G P) H

The inertia subgroup at an unramified prime meets H trivially. Let H be a subgroup of G whose fixed field is F. If P is unramified over 𝓞 F, then the inertia subgroup of P is disjoint from H, since its intersection with H is the inertia subgroup of P over 𝓞 F, of order e(P / 𝓞 F) = 1.

theorem NumberField.pow_index_eq_one_of_ramificationIdx_eq_one {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] {F : Type u_3} [Field F] [Algebra F K] {H : Subgroup G} [H.Normal] [IsGaloisGroup (↥H) F K] {P : Ideal (RingOfIntegers K)} (hP : P.IsPrime) (hunr : P.ramificationIdx (RingOfIntegers F) = 1) {g : G} (hg : g ∈ Ideal.inertia G P) : g ^ H.index = 1

The index of H kills inertia at a prime unramified over the fixed field. If H is a normal subgroup of G with fixed field F and P is unramified over 𝓞 F, then every element of the inertia subgroup at P is killed by H.index: its H.index-th power lies in H, and it lies in the inertia subgroup, which meets H trivially. If the index is infinite, H.index = 0 and the equality is immediate; no finiteness assumption on G is needed.

theorem NumberField.pow_index_eq_one_of_isUnramifiedIn {K : Type u_1} [Field K] [NumberField K] {G : Type u_2} [Group G] [MulSemiringAction G K] [IsGaloisGroup G ℚ K] {F : Type u_3} [Field F] [Algebra F K] [IsMulCommutative G] (H : Subgroup G) [IsGaloisGroup (↥H) F K] (hunr : ∀ (q : Ideal (RingOfIntegers F)), q.IsPrime → Algebra.IsUnramifiedIn (RingOfIntegers K) q) (g : G) : g ^ H.index = 1

An abelian extension of ℚ unramified over a subfield has exponent dividing its degree. Let K be a number field, Galois over ℚ with abelian Galois group G, and let H be a subgroup whose fixed field F has every prime unramified in 𝓞 K. Then g ^ H.index = 1 for every g : G, and H.index is Module.finrank ℚ F by IsGaloisGroup.index_eq_finrank.

Indeed each inertia subgroup is killed by H.index (NumberField.pow_index_eq_one_of_ramificationIdx_eq_one), and in an abelian group the elements killed by a fixed exponent form a subgroup; since the inertia subgroups generate G (NumberField.eq_top_of_forall_inertia_le), that subgroup is all of G.

For F quadratic this says that an abelian extension of ℚ unramified over a quadratic subfield has exponent dividing 2; by Kummer theory over ℚ — not formalised here — such an extension is a compositum of quadratic fields.

theorem NumberField.aut_exponent_dvd_finrank_of_isUnramifiedIn {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] (F : IntermediateField ℚ M) (hunr : ∀ (q : Ideal (RingOfIntegers ↥F)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (RingOfIntegers M) q) : Monoid.exponent Gal(M/ℚ) ∣ Module.finrank ℚ ↥F

An abelian extension unramified over a subfield has exponent dividing its degree. Let M / ℚ be an abelian number-field extension and let F ⊆ M. If every finite prime of F is unramified in M, then Monoid.exponent Gal(M/ℚ) ∣ [F : ℚ].

@[simp]

theorem NumberField.ramifiedPrimes_iSup {K : Type u_1} [Field K] [NumberField K] {ι : Sort u_2} (E : ι → IntermediateField ℚ K) : ramifiedPrimes ↥(⨆ (i : ι), E i) = ⋃ (i : ι), ramifiedPrimes ↥(E i)

The ramified primes of a compositum. Let K be a number field and let E i be intermediate fields of K. A rational prime ramifies in the compositum ⨆ i, E i exactly when it ramifies in one of the E i.

theorem TauCeti.NumberField.exists_mem_inertia_apply_eq_neg {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] {x : K} {c : ℚ} (hx : x ^ 2 = (algebraMap ℚ K) c) {p : ℕ} (hp : p ∈ NumberField.ramifiedPrimes ↥ℚ⟮x⟯) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] : ∃ τ ∈ Ideal.inertia Gal(K/ℚ) Q, τ x = -x

Inertia negates a square root generating a ramified quadratic field. Let K / ℚ be Galois, let x ∈ K square to a rational number, and let p be a prime ramifying in ℚ(x). Then the inertia group of every prime Q of 𝓞 K above p contains an automorphism τ with τ x = -x.