Dirichlet's S-unit rank formula

The S-unit group of a number field has rank r₁ + r₂ - 1 + |S|, for a finite set S of finite places. The general Dedekind-domain rank formula applies because the class group is finite and the ordinary units are finitely generated by Dirichlet's theorem.

When the field F contains the n-th roots of unity, the n-th powers of Fˣ cut out of the S-units a subgroup of index n ^ (r₁ + r₂ + |S|) (TauCeti.relIndex_range_powMonoidHom_sUnits_numberField), that is, n raised to the number of places, infinite ones included, at which an S-unit may have a nontrivial absolute value. By Kummer theory this index is the degree of the extension of F generated by the n-th roots of the S-units, which enters the norm-index computations of global class field theory.

References

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

theorem TauCeti.finrank_sUnits_numberField (F : Type u_1) [Field F] [NumberField F] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) [Finite ↑S] : Module.finrank ℤ (Additive ↥(S.unit F)) = NumberField.Units.rank F + Nat.card ↑S

Dirichlet's S-unit rank formula: allowing denominators at S adds |S| to the unit rank.

theorem TauCeti.relIndex_range_powMonoidHom_sUnits_numberField (F : Type u_1) [Field F] [NumberField F] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F))) [Finite ↑S] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity F n] : (powMonoidHom n).range.relIndex (S.unit F) = n ^ (Fintype.card (NumberField.InfinitePlace F) + Nat.card ↑S)

The index of the n-th powers in the S-units of a number field containing the n-th roots of unity: [U_S : U_S ∩ (Fˣ)ⁿ] = n ^ (r₁ + r₂ + |S|), where r₁ + r₂ is the number of infinite places of F and S is a finite set of finite places.