Idele classes are norms from an extension that splits almost everywhere

Let L/K be an extension of number fields and S a finite set of finite places of K. If at every finite place v ∉ S every unit of K_v is a norm from K_v ⊗[K] L, then every idele class of K is a norm from L: the norm map C_L → C_K is surjective (ideleClassNormMap_surjective_of_forall_range_normUnits_eq_top). This holds in particular when every finite place outside S has a place of L above it with local degree one, for instance when it splits completely in L (ideleClassNormMap_surjective_of_forall_exists_finrank_eq_one).

The proof is weak approximation. Every idele becomes, after multiplication by a principal idele, an n-th power at the places of S and at every infinite place, for any n ≠ 0 (exists_unitEmbedding_mul_mem_range_powMonoidHom): the n-th powers of K_v contain the units congruent to one to a sufficient level, a positive real number is an n-th power, and every complex number is one. With n = [L : K] such a coordinate is the norm of its n-th root, and the placewise norm criterion mem_range_ideleNormMap_iff assembles the local norms into an idele.

This is the norm half of Milne's Proposition 4.6, proved directly rather than through the density of K^× · I^S in I_K. Together with the first fundamental inequality [C_K : N_{L/K} C_L] ≥ [L : K] for cyclic L/K, it shows that a nontrivial solvable extension has infinitely many places that do not split completely. That is how the Frobenius elements of an abelian extension are seen to generate its Galois group without the Chebotarev density theorem, as the Kummer-theoretic proof of the second fundamental inequality requires.

The fixed-field theorems are the norm half of Milne's Proposition 4.7, the step where the Frobenius elements enter. Let L/K be Galois and H a subgroup of Gal(L/K), with fixed field E = L ^ H. If every finite place v ∉ S has a place w of L above it whose decomposition group D(w) lies in H, then the place of E below w has local degree [D(w) : D(w) ∩ H] = 1 over v (IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletion_fixedField), so the norm map C_E → C_K is surjective (ideleClassNormMap_fixedField_surjective_of_stabilizer_le). A subgroup containing every Frobenius element at w contains D(w), so this applies to the subgroup generated by the Frobenius elements at the places outside S (ideleClassNormMap_fixedField_surjective_of_isArithFrobAt_mem).

When H is normal and Gal(L/K) ⧸ H is solvable, a proper H lies in a normal subgroup of prime index, whose fixed field is a cyclic extension of K of prime degree inside E with surjective norm (exists_finrank_prime_ideleClassNormMap_surjective). The first inequality [C_K : N_{E/K}(C_E)] ≥ [E : K] for cyclic E/K excludes such a field, so it forces H = ⊤. Two cases are recorded. If L/K is solvable of degree greater than one and almost every place has a place above it with trivial decomposition group, such a field exists (exists_finrank_prime_ideleClassNormMap_surjective_of_stabilizer_eq_bot): with the first inequality this is Milne's Proposition 4.6. The subgroup generated by the Frobenius elements at the places outside S is normal, since a conjugate of a Frobenius element at w is a Frobenius element at a conjugate of w. So if these Frobenius elements do not generate Gal(L/K) and the quotient by the subgroup they generate is solvable (for instance, L/K is solvable), such a field exists again (exists_finrank_prime_ideleClassNormMap_surjective_of_closure_isArithFrobAt_ne_top): with the first inequality this is Milne's Proposition 4.7, that the Frobenius elements generate Gal(L/K).

The same proof of the second fundamental inequality needs surjectivity in a second situation, where the places outside S need not split (Milne's Proposition 6.10). Let T be a finite set of finite places disjoint from S, where S generates the ideal class group, and let [L : K] divide n. Suppose every element of K_v is a local norm at the places of S and at the infinite places, L has an unramified place above every finite place outside S ∪ T, and the S-units surject onto ∏_{v ∈ T} U_v / U_v ^ n. Then C_L → C_K is again surjective (ideleClassNormMap_surjective_of_forall_exists_mem_unit). Here no approximation is used: an idele class has a representative that is a unit outside S, and an S-unit corrects it to an n-th power at T while preserving the unit condition outside S. The class group and S-unit conditions concern S and T alone (the latter is Milne's Lemma 6.9). The local conditions hold for a Kummer extension L = K(b^{1/n}) of a field containing the n-th roots of unity when b is an n-th power at S and at the infinite places, b is a unit outside S ∪ T, and n is a unit outside S. The first inequality, applied to the cyclic extension L/K, then forces L = K, so b is an n-th power: this is Milne's Proposition 6.10, from which his Lemma 6.7 computes the index of the Kummer idele subgroup in the proof of the second inequality.

Main results

• TauCeti.GlobalNumberFields.exists_unitEmbedding_mul_mem_range_powMonoidHom: every idele is, up to a principal idele, an n-th power at the places of S and at the infinite places.
• TauCeti.Algebra.range_powMonoidHom_le_range_normUnits_baseChange: an [L : K]-th power is a norm from F ⊗[K] L.
• TauCeti.GlobalNumberFields.range_normUnits_adicCompletion_eq_top_of_finrank_eq_one: every unit of K_v is a local norm when some place above v has local degree one.
• TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_range_normUnits_eq_top and TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_exists_finrank_eq_one: the surjectivity of the idele-class norm map.
• TauCeti.GlobalNumberFields.ideleClassNormMap_fixedField_surjective_of_stabilizer_le and TauCeti.GlobalNumberFields.ideleClassNormMap_fixedField_surjective_of_isArithFrobAt_mem: the norm map from the fixed field of a subgroup containing the decomposition groups, or the Frobenius elements, at places above all but finitely many places of K is surjective.
• TauCeti.GlobalNumberFields.exists_finrank_prime_ideleClassNormMap_surjective: if the decomposition groups at places above all but finitely many places of K lie in a proper normal subgroup H with solvable quotient, then L ^ H contains a Galois extension of K of prime degree with surjective idele-class norm map.
• exists_finrank_prime_ideleClassNormMap_surjective_of_stabilizer_eq_bot: the same conclusion for a nontrivial solvable extension in which almost every place splits completely.
• exists_finrank_prime_ideleClassNormMap_surjective_of_closure_isArithFrobAt_ne_top: the same conclusion when the Frobenius elements outside S do not generate the Galois group and the quotient by the subgroup they generate is solvable.
• TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_exists_mem_unit: surjectivity when the S-units surject onto the local power classes of units at T.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 4.5, Proposition 4.6, Proposition 4.7 and Proposition 6.10.

n-th powers at finitely many places

theorem TauCeti.GlobalNumberFields.exists_unitEmbedding_mul_mem_range_powMonoidHom {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {n : ℕ} (hn : n ≠ 0) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ∃ (α : Kˣ), (∀ v ∈ S, v.ideleFiniteCoord ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) α * x) ∈ (powMonoidHom n).range) ∧ ∀ (w : NumberField.InfinitePlace K), w.ideleInfiniteCoord ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) α * x) ∈ (powMonoidHom n).range

Every idele is an n-th power at finitely many places, up to a principal idele. For a finite set S of finite places and n ≠ 0, every idele times a suitable principal idele is an n-th power at each place of S and at each infinite place. This is weak approximation at S and the real places, through exists_unitEmbedding_mul_mem_ideleCongrOneSubgroup for a modulus deep enough at S and divisible by every real place.

Surjectivity of the idele-class norm map

theorem TauCeti.GlobalNumberFields.range_normUnits_adicCompletion_eq_top_of_finrank_eq_one {K : Type u_1} (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) (hw : Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) : (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range = ⊤

Every unit of K_v is a local norm when some place above v has local degree one. The norm from K_v ⊗[K] L is then onto, the factor L_w = K_v alone providing every unit.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_range_normUnits_eq_top {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range = ⊤) : Function.Surjective ⇑(ideleClassNormMap K L)

The idele-class norm map is onto when local norms are onto outside finitely many places. If, at every finite place v of K outside a finite set S, every unit of K_v is a norm from K_v ⊗[K] L, then every idele class of K is the norm of an idele class of L.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_exists_finrank_eq_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) : Function.Surjective ⇑(ideleClassNormMap K L)

Every idele class is a norm from an extension that splits almost everywhere. If every finite place v of K outside a finite set S has a place w of L above it with [L_w : K_v] = 1, for instance because v splits completely in L, then the norm map C_L → C_K is surjective.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_fixedField_surjective_of_stabilizer_le {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (H : Subgroup Gal(L/K)) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), MulAction.stabilizer Gal(L/K) (↑w).asIdeal ≤ H) : Function.Surjective ⇑(ideleClassNormMap K ↥(IntermediateField.fixedField H))

Idele classes are norms from the fixed field of a group containing decomposition groups. Let L/K be Galois and H a subgroup of Gal(L/K). If every finite place v of K outside a finite set S has a place w of L above it whose decomposition group lies in H, then every idele class of K is a norm from the fixed field L ^ H: the place of L ^ H below w has local degree one over v.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_fixedField_surjective_of_isArithFrobAt_mem {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (H : Subgroup Gal(L/K)) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), ∀ (σ : Gal(L/K)), IsArithFrobAt (NumberField.RingOfIntegers K) σ (↑w).asIdeal → σ ∈ H) : Function.Surjective ⇑(ideleClassNormMap K ↥(IntermediateField.fixedField H))

Idele classes are norms from the fixed field of a group containing Frobenius elements. Let L/K be Galois and H a subgroup of Gal(L/K). If every finite place v of K outside a finite set S has a place w of L above it such that H contains every arithmetic Frobenius element at w, then every idele class of K is a norm from the fixed field L ^ H. At a place unramified in L the Frobenius element is unique, so this is the case of the subgroup generated by the Frobenius elements at the places of L outside S, once S contains the ramified places.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_surjective_of_forall_exists_mem_unit {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) {n : ℕ} (hn : Module.finrank K L ∣ n) (hcl : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' ↑S) = ⊤) (hS : ∀ v ∈ S, (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range = ⊤) (hinf : ∀ (w : NumberField.InfinitePlace K), (Algebra.normUnits w.Completion).range = ⊤) (hunr : ∀ v ∉ S, v ∉ T → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) (hT : ∀ (y : (v : ↥T) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)ˣ), (∀ (v : ↥T), Valued.v ↑(y v) = 1) → ∃ u ∈ (↑S).unit K, ∀ (v : ↥T), ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v))) u)⁻¹ * y v ∈ (powMonoidHom n).range) : Function.Surjective ⇑(ideleClassNormMap K L)

Every idele class is a norm when S-units control the local power classes at T (Milne, Class Field Theory, VII, Proposition 6.10). Let S and T be disjoint finite sets of finite places of K, with the classes of the primes of S generating the ideal class group, and let [L : K] divide n. Suppose that

• at the places of S and at the infinite places every element of K_v is a local norm,
• at every finite place outside S ∪ T some place of L above it is unramified, and
• the S-units surject onto ∏_{v ∈ T} U_v / U_v ^ n: every family of local units at T agrees with a single S-unit up to local n-th powers.

Then the norm map C_L → C_K is surjective.

Prime-degree subextensions with surjective norm

theorem TauCeti.GlobalNumberFields.exists_finrank_prime_ideleClassNormMap_surjective {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [H.Normal] [Group.IsSolvable (Gal(L/K) ⧸ H)] (hH : H ≠ ⊤) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), MulAction.stabilizer Gal(L/K) (↑w).asIdeal ≤ H) : ∃ E ≤ IntermediateField.fixedField H, IsGalois K ↥E ∧ Nat.Prime (Module.finrank K ↥E) ∧ Function.Surjective ⇑(ideleClassNormMap K ↥E)

A solvable extension above the decomposition groups contains a prime-degree subextension from which every idele class is a norm. Let L/K be Galois and H a proper normal subgroup of Gal(L/K) with solvable quotient. If every finite place v of K outside a finite set S has a place w of L above it whose decomposition group lies in H, then the fixed field L ^ H contains a Galois extension E/K of prime degree, hence cyclic, with N_{E/K}(C_E) = C_K.

The first fundamental inequality [C_K : N_{E/K}(C_E)] ≥ [E : K] for cyclic E/K rules out such an E, and so rules out such an H.

theorem TauCeti.GlobalNumberFields.exists_finrank_prime_ideleClassNormMap_surjective_of_stabilizer_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [Group.IsSolvable Gal(L/K)] (hL : 1 < Module.finrank K L) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), MulAction.stabilizer Gal(L/K) (↑w).asIdeal = ⊥) : ∃ (E : IntermediateField K L), IsGalois K ↥E ∧ Nat.Prime (Module.finrank K ↥E) ∧ Function.Surjective ⇑(ideleClassNormMap K ↥E)

A nontrivial solvable extension in which almost every place splits completely contains a prime-degree subextension from which every idele class is a norm. Let L/K be a Galois extension of degree greater than one with solvable Galois group. If every finite place v of K outside a finite set S has a place w of L above it with trivial decomposition group, then L contains a Galois extension E/K of prime degree, hence cyclic, with N_{E/K}(C_E) = C_K.

The first fundamental inequality for cyclic extensions rules out such an E, and so shows that a nontrivial solvable extension has infinitely many places that do not split completely.

theorem TauCeti.GlobalNumberFields.exists_finrank_prime_ideleClassNormMap_surjective_of_closure_isArithFrobAt_ne_top {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Group.IsSolvable (Gal(L/K) ⧸ Subgroup.normalClosure {σ : Gal(L/K) | ∃ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers K) σ (↑w).asIdeal})] (hgen : Subgroup.closure {σ : Gal(L/K) | ∃ v ∉ S, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers K) σ (↑w).asIdeal} ≠ ⊤) : ∃ (E : IntermediateField K L), IsGalois K ↥E ∧ Nat.Prime (Module.finrank K ↥E) ∧ Function.Surjective ⇑(ideleClassNormMap K ↥E)

The Frobenius elements outside S generate the Galois group modulo a solvable quotient, unless a prime-degree subextension has surjective norm. Let L/K be Galois and S a finite set of finite places of K. Suppose that the arithmetic Frobenius elements at the places of L above the finite places of K outside S do not generate Gal(L/K), and that the quotient of Gal(L/K) by the normal subgroup they generate is solvable (for instance, L/K is solvable). Then L contains a Galois extension E/K of prime degree, hence cyclic, with N_{E/K}(C_E) = C_K.

The subgroup they generate is normal, since a conjugate of a Frobenius element at w is a Frobenius element at a conjugate of w; so it equals the normal closure used in the solvability hypothesis. The first fundamental inequality for cyclic extensions rules out such an E, and so shows that the Frobenius elements generate Gal(L/K).