Unit power classes at finite places

At a finite place v of a number field K not dividing n, the units of the completed integer ring have as many n-th power classes as there are n-th roots of unity in K_v. If K contains these roots, the count is n, and consequently the product of these unit quotients over a finite set T has n ^ #T elements. This is the local cardinality input to the S-unit surjectivity argument in the Kummer proof of the second fundamental inequality.

The local calculation is TauCeti.card_integerUnitPowerClasses_of_isUnit, transported along the existing identification HeightOneSpectrum.integerEquivAdicCompletionIntegers of the two integer-ring presentations of the completion.

References

• J. S. Milne, Class Field Theory, VII, proof of Lemma 6.9.

theorem IsDedekindDomain.HeightOneSpectrum.finiteIndex_range_powMonoidHom_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} (hn : n ≠ 0) : (powMonoidHom n).range.FiniteIndex

For nonzero n, the n-th powers of the completed integer-ring units have finite index.

instance IsDedekindDomain.HeightOneSpectrum.instFiniteIndexRangePowMonoidHomAdicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} [NeZero n] : (powMonoidHom n).range.FiniteIndex

For nonzero n, the power-map range on completed integer-ring units has finite index.

instance IsDedekindDomain.HeightOneSpectrum.finite_powerClassQuotient_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} [NeZero n] : Finite (TauCeti.powerClassQuotient (↥(adicCompletionIntegers K v))ˣ n)

For nonzero n, the power-class quotient of the completed integer-ring units is finite.

theorem IsDedekindDomain.HeightOneSpectrum.card_unitPowerClasses_adicCompletion {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} (hnv : ↑n ∉ v.asIdeal) : Nat.card ((↥(adicCompletionIntegers K v))ˣ ⧸ (powMonoidHom n).range) = Nat.card ↥(rootsOfUnity n (adicCompletion K v))

At a finite place away from n, the completed integer-ring units have as many n-th power classes as there are n-th roots of unity in the completion.

theorem IsDedekindDomain.HeightOneSpectrum.card_unitPowerClasses_adicCompletion_of_hasEnoughRootsOfUnity {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : ℕ} [HasEnoughRootsOfUnity K n] (hnv : ↑n ∉ v.asIdeal) : Nat.card ((↥(adicCompletionIntegers K v))ˣ ⧸ (powMonoidHom n).range) = n

At a finite place away from n, the completed integer-ring units have n power classes if the number field contains the n-th roots of unity.

theorem TauCeti.GlobalNumberFields.prod_card_unitPowerClasses {K : Type u_1} [Field K] [NumberField K] (n : ℕ) [HasEnoughRootsOfUnity K n] (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hT : ∀ v ∈ T, ↑n ∉ v.asIdeal) : ∏ v ∈ T, Nat.card ((↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))ˣ ⧸ (powMonoidHom n).range) = n ^ T.card

The product of local unit power-class counts. If K contains μ_n and T is a finite set of finite places avoiding n, then the product of the orders of their unit power-class quotients is n ^ #T.