The S-units of ℚ

Let S be a finite set of finite places of ℚ, that is, of height-one primes of 𝓞 ℚ, and for v ∈ S let p_v = Rat.HeightOneSpectrum.natGenerator v be its rational prime. The S-units of ℚ are the rationals ± ∏ p_v ^ n_v. This file computes the general S-unit API of TauCeti.NumberField.SUnit in this case:

• the torsion of the S-units is {±1};
• the primes p_v, v ∈ S, form a fundamental system of S-units, of size NumberField.Units.rank ℚ + #S = #S;
• the S-regulator is ∏ v ∈ S, log p_v. In the determinant formula the omitted infinite place is the only one, and the matrix of the logarithms log |p_u|_v is diagonal with entries log |p_v|_v = -log p_v.

For S = {2} this says that the S-units have rank 1, the fundamental system {2} and the S-regulator log 2. The S-unit 1 / p_v has multiplicative height p_v, all of it carried by the finite place v: its archimedean local factor is 1.

Main results

• Rat.HeightOneSpectrum.mulHeight₁_inv_natGenerator_eq_max_finitePlace and Rat.HeightOneSpectrum.mulHeight₁_inv_natGenerator: the height of 1 / p_v is its local factor at v, which is p_v.
• TauCeti.NumberField.SUnit.mem_torsion_unit_rat_iff: the torsion S-units of ℚ are ±1.
• TauCeti.NumberField.SUnit.finrank_unit_rat: the S-units of ℚ have rank #S.
• TauCeti.NumberField.SUnit.primeUnit: the prime p_v as an S-unit, with TauCeti.NumberField.SUnit.isFundSystem_primeUnit: these primes form a fundamental system.
• TauCeti.NumberField.SUnit.regulator_rat_eq_prod_log: the S-regulator of ℚ is ∏ v ∈ S, log p_v.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, §1.5 (the S-units 1.5.10–1.5.13).

theorem Rat.HeightOneSpectrum.mulHeight₁_inv_natGenerator_eq_max_finitePlace (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) : Height.mulHeight₁ (↑(natGenerator v))⁻¹ = max ((NumberField.FinitePlace.mk v) (↑(natGenerator v))⁻¹) 1

The height of the inverse of the rational prime p of v is carried by the finite place v: 1 / p is a {v}-integer whose archimedean local factor is 1, so its height is its local factor max |1 / p|_v 1 at v.

theorem Rat.HeightOneSpectrum.mulHeight₁_inv_natGenerator (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) : Height.mulHeight₁ (↑(natGenerator v))⁻¹ = ↑(natGenerator v)

The inverse of the rational prime of v has multiplicative height equal to the prime.

theorem TauCeti.NumberField.SUnit.mem_torsion_unit_rat_iff {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))} {x : ↥(S.unit ℚ)} : x ∈ CommGroup.torsion ↥(S.unit ℚ) ↔ ↑↑x = 1 ∨ ↑↑x = -1

The torsion S-units of ℚ are 1 and -1.

theorem TauCeti.NumberField.SUnit.finrank_unit_rat (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) [Finite ↑S] : Module.finrank ℤ (Additive ↥(S.unit ℚ)) = Nat.card ↑S

The S-units of ℚ have rank #S: the unit rank of ℚ is zero.

noncomputable def TauCeti.NumberField.SUnit.primeUnit (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) (v : ↥S) : ↥((↑S).unit ℚ)

The rational prime of a place v ∈ S, as an S-unit of ℚ.

@[simp]

theorem TauCeti.NumberField.SUnit.coe_primeUnit (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) (v : ↥S) : ↑↑(primeUnit S v) = ↑(Rat.HeightOneSpectrum.natGenerator ↑v)

theorem TauCeti.NumberField.SUnit.unitValuation_primeUnit (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))] (v : ↥S) : ((↑S).unitValuation ℚ) (primeUnit S v) = Pi.mulSingle v (Multiplicative.ofAdd (-1))

The valuations at the places of S of the rational prime of v ∈ S are -1 at v and 0 elsewhere, written multiplicatively.

theorem TauCeti.NumberField.SUnit.closure_range_primeUnit_sup_torsion_eq_top (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) : Subgroup.closure (Set.range (primeUnit S)) ⊔ CommGroup.torsion ↥((↑S).unit ℚ) = ⊤

The rational primes of the places of S, together with ±1, generate the S-units of ℚ.

theorem TauCeti.NumberField.SUnit.isFundSystem_primeUnit (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) : IsFundSystem (↑S) (primeUnit S)

The rational primes of the places of S form a fundamental system of S-units of ℚ.

theorem TauCeti.NumberField.SUnit.regulator_rat_eq_prod_log (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) : regulator S = ∏ v ∈ S, Real.log ↑(Rat.HeightOneSpectrum.natGenerator v)

The S-regulator of ℚ is the product of the logarithms of the rational primes of the places of S. For S = {2} it is log 2.