The rank of the S-unit group

For a Dedekind domain with finite class group, the valuations of the S-units form a finite-index subgroup of the integer tuples indexed by a finite set S of primes. Consequently, the rank of the S-unit group is the rank of the ordinary unit group plus the cardinality of S. This supplies the rank calculation for the unit lattices used in norm-index computations.

The rank then counts the n-th powers: the n-th powers of Kˣ cut out of the S-units a subgroup of index n ^ (rank Rˣ + |S|) · #μₙ(K) (TauCeti.relIndex_range_powMonoidHom_sUnits). For K a number field containing the n-th roots of unity this is the degree of the Kummer extension generated by the n-th roots of the S-units.

We use Mathlib's Set.unit and the valuation map Set.unitValuation. The finite-index assertion comes from raising a fractional ideal supported on S to the class number: it then has a generator which is an S-unit.

References

• J. S. Milne, Class Field Theory, Chapter VII, §4 (the S-unit lattices).

theorem TauCeti.pow_mem_range_unitValuation (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) [Finite ↑S] (n : ℕ) (hn : ∀ (c : ClassGroup R), c ^ n = 1) (f : ↑S → Multiplicative ℤ) : f ^ n ∈ (S.unitValuation K).range

If n annihilates the class group, every tuple of S-valuations raised to n is the valuation of an S-unit.

theorem TauCeti.finiteIndex_range_unitValuation (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Finite (ClassGroup R)] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) [Finite ↑S] : (S.unitValuation K).range.FiniteIndex

For a finite set S and finite class group, the S-unit valuation lattice has finite index in the integer tuples on S.

theorem TauCeti.finrank_sUnits (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Finite (ClassGroup R)] [Monoid.FG Rˣ] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) [Finite ↑S] : Module.finrank ℤ (Additive ↥(S.unit K)) = Module.finrank ℤ (Additive Rˣ) + Nat.card ↑S

The S-unit rank is the ordinary unit rank plus the number of allowed primes, provided the class group is finite and the ordinary units are finitely generated.

theorem TauCeti.relIndex_range_powMonoidHom_sUnits (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Finite (ClassGroup R)] [Monoid.FG Rˣ] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) [Finite ↑S] (n : ℕ) [NeZero n] : (powMonoidHom n).range.relIndex (S.unit K) = n ^ (Module.finrank ℤ (Additive Rˣ) + Nat.card ↑S) * Nat.card ↥(rootsOfUnity n K)

The index of the n-th powers of Kˣ in the S-units: [U_S : U_S ∩ (Kˣ)ⁿ] = n ^ (rank Rˣ + |S|) · #μₙ(K), provided the class group is finite and the ordinary units are finitely generated. The n-th powers of Kˣ meet the S-units in the n-th powers of S-units (Set.range_powMonoidHom_subgroupOf_unit), whose index in the finitely generated group U_S is counted by its rank (finrank_sUnits) and its n-torsion, which is μₙ(K) (Set.natCard_ker_powMonoidHom_unit).

instance TauCeti.isFiniteRelIndex_range_powMonoidHom_sUnits (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Finite (ClassGroup R)] [Monoid.FG Rˣ] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) [Finite ↑S] (n : ℕ) [NeZero n] : (powMonoidHom n).range.IsFiniteRelIndex (S.unit K)

For a finite set S of primes, the n-th powers of Kˣ cut out of the S-units a subgroup of finite index, provided the class group is finite and the ordinary units are finitely generated.