Powers of S-units

Let R be a Dedekind domain with fraction field K and S a set of height-one primes of R. The value group of each v-adic valuation is torsion-free, so an element of Kˣ is an S-unit as soon as one of its nonzero powers is (Set.pow_mem_unit_iff). Two consequences describe the n-th power map on the group Set.unit S K of S-units:

• its kernel is the whole group μₙ(K) of n-th roots of unity of K, every root of unity being an S-unit (Set.rootsOfUnity_le_unit, Set.ker_powMonoidHom_unit);
• an S-unit that is an n-th power in Kˣ is the n-th power of an S-unit, so the subgroup (Kˣ)ⁿ cuts out of the S-units exactly their own n-th powers (Set.range_powMonoidHom_subgroupOf_unit).

Together they reduce the index [U_S : U_S ∩ (Kˣ)ⁿ] to the index of the n-th powers inside the finitely generated group U_S, which TauCeti.relIndex_range_powMonoidHom_sUnits computes. When K contains the n-th roots of unity and n is invertible in K, this index is the degree of the Kummer extension of K generated by the n-th roots of the S-units.

Main results

• Set.pow_mem_unit_iff: for n ≠ 0, xⁿ is an S-unit iff x is.
• Set.rootsOfUnity_le_unit: every n-th root of unity of K is an S-unit.
• Set.range_powMonoidHom_subgroupOf_unit: the n-th powers of Kˣ that are S-units are the n-th powers of S-units.
• Set.ker_powMonoidHom_unit and Set.natCard_ker_powMonoidHom_unit: the n-torsion of the S-units is the group of n-th roots of unity of K.

References

• J. S. Milne, Class Field Theory, Chapter VII, §5 (the Kummer extension generated by the roots of the S-units).

theorem Set.pow_mem_unit_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} (hn : n ≠ 0) {x : Kˣ} : x ^ n ∈ S.unit K ↔ x ∈ S.unit K

An element of Kˣ is an S-unit as soon as a nonzero power of it is: away from S, a valuation whose n-th power is trivial is itself trivial.

theorem Set.rootsOfUnity_le_unit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) [NeZero n] : rootsOfUnity n K ≤ S.unit K

Every n-th root of unity of K is an S-unit, for every S.

theorem Set.range_powMonoidHom_subgroupOf_unit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : (powMonoidHom n).range.subgroupOf (S.unit K) = (powMonoidHom n).range

An S-unit that is an n-th power in Kˣ is the n-th power of an S-unit: read in the S-units, the subgroup (Kˣ)ⁿ is the subgroup of n-th powers of S-units.

theorem Set.ker_powMonoidHom_unit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) : (powMonoidHom n).ker = (rootsOfUnity n K).subgroupOf (S.unit K)

The n-torsion of the S-units consists of the n-th roots of unity of K that are S-units; by rootsOfUnity_le_unit these are all of them when n ≠ 0.

theorem Set.natCard_ker_powMonoidHom_unit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (n : ℕ) [NeZero n] : Nat.card ↥(powMonoidHom n).ker = Nat.card ↥(rootsOfUnity n K)

The n-torsion of the S-units has as many elements as the group μₙ(K) of n-th roots of unity of K.