Dirichlet's unit theorem in structural form

Mathlib's NumberField.Units.exist_unique_eq_mul_prod states that every unit of 𝓞 F has a unique decomposition as a root of unity times a product of powers of the fundamental system. This file packages that unique decomposition as a multiplicative equivalence

(𝓞 F)ˣ ≃* torsion F × Multiplicative (Fin (rank F) → ℤ),

exhibiting the unit group as the product of its (finite cyclic) torsion subgroup and a free abelian group of Dirichlet rank. This structural form is what downstream counting arguments consume — for instance the exact number of unit square classes in TauCeti.NumberTheory.NumberField.Units.ElementaryTwoQuotient.

Main results

• NumberField.unitsMulEquivTorsionProdMultiplicative: the unit group as the product of its torsion subgroup and the free abelian group on the fundamental system.
• NumberField.rank_eq_one_of_finrank_eq_two_of_isReal: a quadratic field with a real place has unit rank one.
• NumberField.rank_add_nrComplexPlaces_add_one: the unit rank plus the number of complex places plus one is the degree.

noncomputable def NumberField.unitsMulEquivTorsionProdMultiplicative (F : Type u_1) [Field F] [NumberField F] : (RingOfIntegers F)ˣ ≃* ↥(Units.torsion F) × Multiplicative (Fin (Units.rank F) → ℤ)

Dirichlet's unit theorem, structural form. The unit group of the ring of integers of a number field is the product of its torsion subgroup and the free abelian group generated by the fundamental system: a unit corresponds to its unique decomposition as a root of unity times a product of powers of fundamental units (NumberField.Units.exist_unique_eq_mul_prod).

Equations

• NumberField.unitsMulEquivTorsionProdMultiplicative F = (MulEquiv.ofBijective (NumberField.torsionProdMultiplicativeToUnits✝ F) ⋯).symm

@[simp]

theorem NumberField.unitsMulEquivTorsionProdMultiplicative_symm_apply (F : Type u_1) [Field F] [NumberField F] (ζ : ↥(Units.torsion F)) (e : Multiplicative (Fin (Units.rank F) → ℤ)) : (unitsMulEquivTorsionProdMultiplicative F).symm (ζ, e) = ↑ζ * ∏ i : Fin (Units.rank F), Units.fundSystem F i ^ Multiplicative.toAdd e i

The inverse of NumberField.unitsMulEquivTorsionProdMultiplicative sends a pair to the root of unity times the product of powers of fundamental units.

@[simp]

theorem NumberField.unitsMulEquivTorsionProdMultiplicative_apply (F : Type u_1) [Field F] [NumberField F] (ζ : ↥(Units.torsion F)) (e : Fin (Units.rank F) → ℤ) : (unitsMulEquivTorsionProdMultiplicative F) (↑ζ * ∏ i : Fin (Units.rank F), Units.fundSystem F i ^ e i) = (ζ, Multiplicative.ofAdd e)

The forward map of NumberField.unitsMulEquivTorsionProdMultiplicative reads off the Dirichlet decomposition: a unit presented as a root of unity ζ times a product of powers of the fundamental system is sent to the pair (ζ, e).

theorem NumberField.rank_add_nrComplexPlaces_add_one (F : Type u_1) [Field F] [NumberField F] : Units.rank F + InfinitePlace.nrComplexPlaces F + 1 = Module.finrank ℚ F

The unit rank, the complex places and one exhaust the degree. Dirichlet's rank is #(InfinitePlace F) - 1 while the degree is r₁ + 2 * r₂, so restoring the complex places and the one place the rank drops recovers finrank ℚ F.

Stated as an addition rather than as rank F + nrComplexPlaces F = finrank ℚ F - 1: the subtraction on ℕ is truncated, and the additive form needs no positivity side condition.

theorem NumberField.rank_eq_one_of_finrank_eq_two_of_isReal {F : Type u_2} [Field F] [NumberField F] (hdeg : Module.finrank ℚ F = 2) {w : InfinitePlace F} (hw : w.IsReal) : Units.rank F = 1

A real quadratic field has unit rank one. In degree two, a real infinite place forces both infinite places to be real, so the unit rank is 2 - 1 = 1.