Power classes at the places of a number field

Let K be a number field and n ≥ 1. At every place v of K, finite or infinite, the number of n-th power classes of the completion is

#(K_vˣ ⧸ (K_vˣ)ⁿ) · ‖n‖_v = n · #μ_n(K_v),

where ‖·‖_v is the normalized absolute value TauCeti.GlobalNumberFields.normalizedAbsValue and μ_n(K_v) is the group of n-th roots of unity of K_v. At a finite place this is the local count TauCeti.card_powerClasses_eq_mul_inv_normalizedAbsoluteValue, once the norm of K_v is identified with the normalized absolute value of K_v as a nonarchimedean local field. At a real place it is TauCeti.card_powerClasses_real, #(ℝˣ ⧸ (ℝˣ)ⁿ) = #μ_n(ℝ), and at a complex place it is TauCeti.card_powerClasses_of_isAlgClosed: every unit is an n-th power.

If K contains the n-th roots of unity, every factor #μ_n(K_v) is n. Let S be a finite set of finite places containing those above the primes dividing n. Then ‖n‖_v = 1 at the finite places outside S, so the product formula turns the local counts into the global identity

∏_{v ∈ S} #(K_vˣ ⧸ (K_vˣ)ⁿ) · ∏_{w | ∞} #(K_wˣ ⧸ (K_wˣ)ⁿ) = n ^ (2 (#S + r₁ + r₂)).

The left side is the index, in the S-ideles, of the subgroup of ideles that are n-th powers at the places of S and at the infinite places and units elsewhere. That index is the local input to the Kummer case of the second fundamental inequality and of the global existence theorem, where it is compared with the index n ^ (#S + r₁ + r₂) of the n-th powers in the S-units.

Main results

• IsDedekindDomain.HeightOneSpectrum.coe_normalizedAbsoluteValue_adicCompletion: the norm of K_v is its normalized absolute value as a nonarchimedean local field.
• IsDedekindDomain.HeightOneSpectrum.card_powerClasses_adicCompletion_mul_normalizedAbsValue and NumberField.InfinitePlace.card_powerClasses_completion_mul_normalizedAbsValue: the local count #(K_vˣ ⧸ (K_vˣ)ⁿ) · ‖n‖_v = n · #μ_n(K_v) at a finite and at an infinite place.
• TauCeti.GlobalNumberFields.prod_card_powerClasses: the product of the local counts over S and the infinite places is n ^ (2 (#S + r₁ + r₂)) when μ_n ⊆ K.

References

• J. S. Milne, Class Field Theory, VII, §5 (the second inequality in the Kummer case).
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter VII, §6.

theorem IsDedekindDomain.HeightOneSpectrum.coe_normalizedAbsoluteValue_adicCompletion {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : adicCompletion K v) : ↑((TauCeti.normalizedAbsoluteValue (adicCompletion K v)) x) = ‖x‖

The norm of the completion K_v of a number field is its normalized absolute value as a nonarchimedean local field: both send a nonzero x to (N v) ^ (-v(x)), the residue field of K_v having N v elements.

theorem IsDedekindDomain.HeightOneSpectrum.card_powerClasses_adicCompletion_mul_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} (hn : n ≠ 0) : ↑(Nat.card ((adicCompletion K v)ˣ ⧸ (powMonoidHom n).range)) * (TauCeti.GlobalNumberFields.normalizedAbsValue (Sum.inl v)) ↑n = ↑n * ↑(Nat.card ↥(rootsOfUnity n (adicCompletion K v)))

The power classes at a finite place. For n ≠ 0 and a finite place v of a number field K, #(K_vˣ ⧸ (K_vˣ)ⁿ) · ‖n‖_v = n · #μ_n(K_v).

theorem NumberField.InfinitePlace.card_powerClasses_completion_mul_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] (w : InfinitePlace K) {n : ℕ} (hn : n ≠ 0) : ↑(Nat.card (w.Completionˣ ⧸ (powMonoidHom n).range)) * (TauCeti.GlobalNumberFields.normalizedAbsValue (Sum.inr w)) ↑n = ↑n * ↑(Nat.card ↥(rootsOfUnity n w.Completion))

The power classes at an infinite place. For n ≠ 0 and an infinite place w of a number field K, #(K_wˣ ⧸ (K_wˣ)ⁿ) · ‖n‖_w = n · #μ_n(K_w), where ‖n‖_w is n at a real place and n ^ 2 at a complex place.

theorem TauCeti.GlobalNumberFields.prod_card_powerClasses {K : Type u_1} [Field K] [NumberField K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑n ∈ v.asIdeal → v ∈ S) : (∏ v ∈ S, Nat.card ((IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ ⧸ (powMonoidHom n).range)) * ∏ w : NumberField.InfinitePlace K, Nat.card (w.Completionˣ ⧸ (powMonoidHom n).range) = n ^ (2 * (S.card + Fintype.card (NumberField.InfinitePlace K)))

The product of the local power indices. Let K be a number field containing the n-th roots of unity and let S be a finite set of finite places of K containing every place above a prime dividing n. Then the product of the numbers of n-th power classes of the completions of K at the places of S and at the infinite places is n ^ (2 (#S + r₁ + r₂)), where r₁ + r₂ is the number of infinite places.