15.5. Units🔗

The unit group of the ring of integers is the group of units (𝓞 K)ˣ:

open NumberField

(𝓞 K)ˣ : Type u_1#check ((𝓞 K)ˣ : Type _)

Dirichlet's unit theorem describes its structure: (𝓞 K)ˣ is a finitely generated abelian group, the product of a finite torsion subgroup and a free part of rank r₁ + r₂ - 1, where r₁ and r₂ count the real and complex places.

The unit group is written multiplicatively, but Dirichlet's theorem is a statement about it as a ℤ-module, so Mathlib phrases the rank through Additive, which reinterprets a multiplicative group additively. Finiteness as a module is an instance,

example : Module.Finite ℤ (Additive (𝓞 K)ˣ) :=
  inferInstance

and its rank is NumberField.Units.finrank_eq, where the right-hand side NumberField.Units.rank is defined as card (InfinitePlace K) - 1 = r₁ + r₂ - 1:

Units.finrank_eq K : finrank ℤ (Additive (𝓞 K)ˣ) = Units.rank K#check (NumberField.Units.finrank_eq K)

Two further invariants attached to the units are the regulator NumberField.Units.regulator, the covolume of the unit lattice,

Units.regulator K : ℝ#check (NumberField.Units.regulator K : ℝ)

and the order of the torsion subgroup (the roots of unity in K), NumberField.Units.torsionOrder:

Units.torsionOrder K : ℕ#check (NumberField.Units.torsionOrder K : ℕ)