Fundamental systems of S-units

For a finite set S of finite places of a number field, the group of S-units modulo its torsion subgroup is free of rank NumberField.Units.rank K + Nat.card S. Choosing a basis and lifting it gives a fundamental system of S-units. Every S-unit then has a unique expression as a torsion element times a product of integral powers of the fundamental system.

This is the decomposition form of Dirichlet's S-unit theorem. It supplies the generators whose logarithms form a basis of the S-unit lattice and on which the S-regulator is evaluated.

The construction follows Mathlib's ordinary-unit API in Mathlib.NumberTheory.NumberField.Units.DirichletTheorem, especially NumberField.Units.basisModTorsion, NumberField.Units.fundSystem, and NumberField.Units.exist_unique_eq_mul_prod. The corresponding S-unit formalization also appears in Ralf Stephan's ArithmeticHeights/SUnitTheorem.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06, released under Apache 2.0.

Main definitions and results

• TauCeti.NumberField.SUnit.basisModTorsion: a basis of the S-units modulo torsion.
• TauCeti.NumberField.SUnit.fundSystem: arbitrary lifts of that basis to S-units.
• TauCeti.NumberField.SUnit.exist_unique_eq_mul_prod: unique decomposition of an S-unit into its torsion and free parts.
• TauCeti.NumberField.SUnit.closure_fundSystem_sup_torsion_eq_top: the fundamental system and torsion generate all S-units.
• TauCeti.NumberField.SUnit.IsFundSystem: an arbitrary family of S-units is a fundamental system: it has the right number of members and generates the S-units modulo torsion.
• TauCeti.NumberField.SUnit.isFundSystem_iff: a family is a fundamental system exactly when its classes form a basis of the S-units modulo torsion.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Theorem 1.5.13.

noncomputable def TauCeti.NumberField.SUnit.basisModTorsion {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Module.Basis (Fin (NumberField.Units.rank K + Nat.card ↑S)) ℤ (Additive ↥(S.unit K) ⧸ Submodule.torsion ℤ (Additive ↥(S.unit K)))

A basis of the group of S-units modulo its torsion submodule.

noncomputable def TauCeti.NumberField.SUnit.fundSystem {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Fin (NumberField.Units.rank K + Nat.card ↑S) → ↥(S.unit K)

A fundamental system of S-units, obtained by lifting basisModTorsion through the quotient by torsion.

@[simp]

theorem TauCeti.NumberField.SUnit.fundSystem_mk {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] (i : Fin (NumberField.Units.rank K + Nat.card ↑S)) : Submodule.Quotient.mk (Additive.ofMul (fundSystem S i)) = (basisModTorsion S) i

The image of a fundamental S-unit in the quotient by torsion is the corresponding basis vector.

theorem TauCeti.NumberField.SUnit.fun_eq_repr {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] {x ζ : ↥(S.unit K)} {f : Fin (NumberField.Units.rank K + Nat.card ↑S) → ℤ} (hζ : ζ ∈ CommGroup.torsion ↥(S.unit K)) (h : x = ζ * ∏ i : Fin (NumberField.Units.rank K + Nat.card ↑S), fundSystem S i ^ f i) : f = ⇑((basisModTorsion S).repr (Submodule.Quotient.mk (Additive.ofMul x)))

The exponents in any torsion-times-fundamental-system expression are the basis coordinates of the S-unit modulo torsion.

theorem TauCeti.NumberField.SUnit.exist_unique_eq_mul_prod {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] (x : ↥(S.unit K)) : ∃! ζe : ↥(CommGroup.torsion ↥(S.unit K)) × (Fin (NumberField.Units.rank K + Nat.card ↑S) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K + Nat.card ↑S), fundSystem S i ^ ζe.2 i

Every S-unit has a unique expression as a torsion S-unit times a product of integral powers of the fundamental system.

theorem TauCeti.NumberField.SUnit.closure_fundSystem_sup_torsion_eq_top {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Subgroup.closure (Set.range (fundSystem S)) ⊔ CommGroup.torsion ↥(S.unit K) = ⊤

The fundamental system and the torsion subgroup generate the full group of S-units.

Arbitrary fundamental systems

structure TauCeti.NumberField.SUnit.IsFundSystem {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {ι : Type u_2} (ε : ι → ↥(S.unit K)) : Prop

A family ε of S-units is a fundamental system if it is indexed by a finite type with NumberField.Units.rank K + Nat.card S elements and, together with the torsion subgroup, generates the group of S-units.

• finite : Finite ι

  The family is finite.

• card_eq : Nat.card ι = NumberField.Units.rank K + Nat.card ↑S

  The family has NumberField.Units.rank K + Nat.card S members.

• closure_sup_torsion_eq_top : Subgroup.closure (Set.range ε) ⊔ CommGroup.torsion ↥(S.unit K) = ⊤

  The family and the torsion subgroup generate the group of S-units.

theorem TauCeti.NumberField.SUnit.isFundSystem_fundSystem {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : IsFundSystem S (fundSystem S)

The chosen family TauCeti.NumberField.SUnit.fundSystem is a fundamental system.

theorem TauCeti.NumberField.SUnit.isFundSystem_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} [Finite ↑S] {ι : Type u_2} (ε : ι → ↥(S.unit K)) : IsFundSystem S ε ↔ (LinearIndependent ℤ fun (i : ι) => Submodule.Quotient.mk (Additive.ofMul (ε i))) ∧ Submodule.span ℤ (Set.range fun (i : ι) => Submodule.Quotient.mk (Additive.ofMul (ε i))) = ⊤

A family of S-units is a fundamental system exactly when its classes modulo torsion form a basis of the S-units modulo torsion.