Idele norms from a Galois extension of exponent n

Let L/K be a finite Galois extension of number fields such that n kills Gal(L/K), for instance a Kummer extension K(Δ^{1/n}) of a field containing the n-th roots of unity. This file shows that the ideles of the following shape are norms of ideles of L:

∏_{v ∈ S} (K_vˣ)ⁿ × ∏_{v ∈ T} K_vˣ × ∏_{v ∉ S ∪ T} 𝒪_vˣ × ∏_{v ∣ ∞} (K_vˣ)ⁿ,

where L/K is unramified at the finite places outside S ∪ T and the places of T split completely in L. By the placewise criterion GlobalNumberFields.mem_range_ideleNormMap_iff it is enough to treat one place at a time.

• At a finite place, the local Galois group Gal(L_w/K_v) is the decomposition group of w, a subgroup of Gal(L/K), so n kills it, and local reciprocity makes every n-th power a norm (powerSubgroup_le_normGroup_of_exponent_dvd).
• At an infinite place, the local degree [L_w : K_v] is the order of the decomposition group, which is 1 or 2; that group is cyclic, so its order divides n and every n-th power is a power of a ^ [L_w : K_v] = N_{L_w/K_v}(a) (TauCeti.pow_mem_range_normUnits_completion).
• At a place outside S ∪ T, units are norms from the unramified completions (TauCeti.exists_unit_preimages_of_isUnramifiedAt).
• At a place of local degree one, every element is a norm (TauCeti.mem_range_normUnits_adicCompletion_of_finrank_eq_one).

This is the inclusion of the "Kummer idele subgroup" in the norms of the Kummer extension, the norm half of the computation of the norm index of a Kummer extension through S-units in the proof of the second fundamental inequality and of global existence.

For a global element the finite and infinite cases combine: every n-th power in Kˣ is a norm at every place (isLocalNormEverywhere_pow_of_exponent_dvd). For a biquadratic extension, n = 2, this is the local half of the failure of the Hasse norm principle: squares are local norms everywhere, but need not be global norms.

Main results

• TauCeti.ClassFieldTheory.pow_mem_range_normUnits_adicCompletion: at a finite place every n-th power is a local norm.
• TauCeti.ClassFieldTheory.mem_range_ideleNormMap_of_exponent_dvd: the ideles displayed above are idele norms from L.
• TauCeti.ClassFieldTheory.isLocalNormEverywhere_pow_of_exponent_dvd: every n-th power of Kˣ is a local norm everywhere.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §5 (the second inequality through Kummer theory) and §9 (the existence theorem).

theorem TauCeti.ClassFieldTheory.pow_mem_range_normUnits_adicCompletion (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : a ^ n ∈ (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range

n-th powers are local norms at a finite place. If n kills Gal(L/K), then every n-th power of K_vˣ is a norm from the local étale algebra K_v ⊗[K] L: the local Galois group at a place above v is a decomposition group, so n kills it too, and local reciprocity applies.

theorem TauCeti.ClassFieldTheory.mem_range_ideleNormMap_of_exponent_dvd (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) {S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hT : ∀ v ∈ T, ∃ (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) (hU : ∀ v ∉ S, v ∉ T → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hxS : ∀ v ∈ S, v.ideleFiniteCoord x ∈ powerSubgroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ n) (hxU : ∀ v ∉ S, v ∉ T → Valued.v ↑(v.ideleFiniteCoord x) = 1) (hxinf : ∀ (v : NumberField.InfinitePlace K), v.ideleInfiniteCoord x ∈ powerSubgroup v.Completionˣ n) : x ∈ (GlobalNumberFields.ideleNormMap K L).range

Idele norms from a Galois extension of exponent n. Let L/K be a finite Galois extension of number fields such that n kills Gal(L/K). Let S and T be sets of finite places of K such that each place of T has a completion of L above it of degree one, and each finite place outside S ∪ T has an unramified place of L above it. Then an idele of K is the norm of an idele of L as soon as its coordinates are n-th powers at the places of S and at the infinite places, and units at the finite places outside S ∪ T.

theorem TauCeti.ClassFieldTheory.isLocalNormEverywhere_pow_of_exponent_dvd (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (x : Kˣ) : GlobalNumberFields.IsLocalNormEverywhere K L (x ^ n)

n-th powers are local norms everywhere. If n kills Gal(L/K), then for every x ∈ Kˣ the power xⁿ is a norm from the local étale algebra K_v ⊗[K] L at every finite and every infinite place v of K.