Documentation

TauCeti.NumberTheory.NumberField.SUnits.Rat.Structure

Rational S-units #

For a finite set S of natural numbers, the rational S-units are Mathlib's Set.unit S' β„š, where S' is the set of height-one primes v of π“ž β„š whose rational prime Rat.HeightOneSpectrum.primesEquiv v lies in S. Thus x ∈ U_S exactly when x is a unit at every prime outside S. This file makes the group explicit.

Main results #

The sign, product and height descriptions need S to consist of primes: for S = {4} the set S' is empty, so U_S = {±1}, while 4 = ∏_{p ∈ S} p ^ 1.

References #

source
theorem TauCeti.mem_sUnits_rat_iff_forall_padicValRat_eq_zero {S : Set β„•} {x : β„šΛ£} :
x ∈ {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š ↔ βˆ€ (p : β„•), Nat.Prime p β†’ p βˆ‰ S β†’ padicValRat p ↑x = 0

A nonzero rational number is an S-unit exactly when its p-adic valuation vanishes at every prime p βˆ‰ S. Here S is an arbitrary set of natural numbers.

source
theorem TauCeti.mem_sUnits_rat_iff_num_den {S : Finset β„•} {x : β„šΛ£} :
x ∈ {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š ↔ (↑x).num.natAbs ∈ Nat.factoredNumbers S ∧ (↑x).den ∈ Nat.factoredNumbers S

Rational S-units through numerator and denominator. A rational number is an S-unit exactly when the absolute value of its numerator and its denominator are S-factored, i.e. have all their prime factors in S.

source
instance TauCeti.finite_setOf_primesEquiv_mem {S : Finset β„•} :
Finite ↑{v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}

Only finitely many height-one primes of π“ž β„š correspond to rational primes in a finite set S, so the rational S-units are those of a finite set of places.

source
theorem TauCeti.sUnits_rat_fg {S : Finset β„•} :
Group.FG β†₯({v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š)

The rational S-units are finitely generated. This holds for every finite set S of natural numbers; only the primes in S contribute.

source
noncomputable def TauCeti.sUnitsRatMulEquiv {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) :
β†₯({v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š) ≃* β„€Λ£ Γ— Multiplicative (β†₯S β†’ β„€)

The structure of the rational S-units. If S consists of primes, the map x ↦ (sign x, (v_p(x))_{p ∈ S}) is an isomorphism from the rational S-units to β„€Λ£ Γ— Multiplicative (S β†’ β„€); its inverse sends (Ξ΅, z) to Ξ΅ ∏_{p ∈ S} p ^ z_p (TauCeti.coe_sUnitsRatMulEquiv_symm_apply).

Instances For
    source
    @[simp]
    theorem TauCeti.coe_sUnitsRatMulEquiv_apply_fst {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) (x : β†₯({v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š)) :
    ↑((sUnitsRatMulEquiv hS) x).1 = ↑(SignType.sign ↑↑x)

    The first component of sUnitsRatMulEquiv is the sign.

    source
    @[simp]
    theorem TauCeti.toAdd_sUnitsRatMulEquiv_apply_snd {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) (x : β†₯({v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š)) (p : β†₯S) :
    Multiplicative.toAdd ((sUnitsRatMulEquiv hS) x).2 p = padicValRat ↑p ↑↑x

    The second component of sUnitsRatMulEquiv records the p-adic valuations at p ∈ S.

    source
    @[simp]
    theorem TauCeti.coe_sUnitsRatMulEquiv_symm_apply {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) (w : β„€Λ£ Γ— Multiplicative (β†₯S β†’ β„€)) :
    ↑↑((sUnitsRatMulEquiv hS).symm w) = ↑↑w.1 * ∏ p : β†₯S, ↑↑p ^ Multiplicative.toAdd w.2 p

    The inverse of sUnitsRatMulEquiv sends (Ρ, z) to Ρ ∏_{p ∈ S} p ^ z_p.

    source
    theorem TauCeti.mem_sUnits_rat_iff_eq_sign_mul_prod {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) {x : β„šΛ£} :
    x ∈ {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š ↔ βˆƒ (Ξ΅ : β„€Λ£) (z : β†₯S β†’ β„€), ↑x = ↑↑Ρ * ∏ p : β†₯S, ↑↑p ^ z p

    Rational S-units as signed products of prime powers. If S consists of primes, a rational number is an S-unit exactly when it is Ξ΅ ∏_{p ∈ S} p ^ z_p for a sign Ξ΅ ∈ β„€Λ£ and integer exponents z.

    source
    theorem TauCeti.finrank_sUnits_rat {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) :
    Module.finrank β„€ (Additive β†₯({v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š)) = S.card

    The rank of the rational S-units. If S consists of primes, the group of rational S-units has rank |S|.

    source
    theorem TauCeti.mulHeight₁_sUnits_rat {S : Finset β„•} (hS : βˆ€ p ∈ S, Nat.Prime p) {x : β„šΛ£} (hx : x ∈ {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers β„š) | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit β„š) :
    Height.mulHeight₁ ↑x = max (∏ p ∈ S, ↑p ^ (padicValRat p ↑x).toNat) (∏ p ∈ S, ↑p ^ (-padicValRat p ↑x).toNat)

    The height of a rational S-unit. If S consists of primes and x is an S-unit, then H(x) = max (∏_{p ∈ S} p ^ max(v_p(x), 0)) (∏_{p ∈ S} p ^ max(-v_p(x), 0)): the two products are the absolute value of the numerator and the denominator of x.