Documentation

TauCeti.NumberTheory.NumberField.SUnits.LogEmbedding

The logarithmic embedding of S-units #

For a finite set S of finite places of a number field, the logarithmic embedding sends an S-unit to its weighted logarithms at all infinite places except Mathlib's distinguished place, together with its logarithms at the places in S. The product formula recovers the omitted infinite coordinate as minus the sum of these coordinates.

The product formula needs the S-unit hypothesis: 2 is an S-integer for S = ∅, but its weighted logarithms at the infinite places sum to [K : ℚ] * log 2, so it is not an ∅-unit.

Ordinary units map to the usual Dirichlet logarithmic embedding in the infinite coordinates and to zero in the finite coordinates. These facts are the coordinate foundation for the S-logarithmic lattice and its regulator.

References #

source
@[reducible, inline]
abbrev TauCeti.NumberField.SUnit.logSpace {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
Type u_1

The logarithmic space for the S-units, with the coordinate at the distinguished infinite place omitted.

Instances For
    source
    noncomputable def TauCeti.NumberField.SUnit.logEmbedding {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
    Additive ↥((↑S).unit K) →+ logSpace S

    The logarithmic embedding of the S-units. Its infinite coordinates are weighted by the place multiplicity, while its finite coordinates use the normalized finite-place absolute values.

    Instances For
      source
      @[simp]
      theorem TauCeti.NumberField.SUnit.logEmbedding_apply_inl {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ↥((↑S).unit K)) (w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) :
      (logEmbedding S) (Additive.ofMul x) (Sum.inl w) = ↑(↑w).mult * Real.log (↑w ↑↑x)
      source
      @[simp]
      theorem TauCeti.NumberField.SUnit.logEmbedding_apply_inr {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ↥((↑S).unit K)) (v : ↥S) :
      (logEmbedding S) (Additive.ofMul x) (Sum.inr v) = Real.log ((NumberField.FinitePlace.mk ↑v) ↑↑x)
      source
      theorem TauCeti.NumberField.SUnit.sum_mult_mul_log_add_sum_log_finitePlace {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ↥((↑S).unit K)) :
      ∑ w : NumberField.InfinitePlace K, ↑w.mult * Real.log (w ↑↑x) + ∑ v : ↥S, Real.log ((NumberField.FinitePlace.mk ↑v) ↑↑x) = 0

      The product formula for an S-unit, with the finite contribution restricted to S.

      The product formula needs the S-unit hypothesis #

      source
      theorem TauCeti.NumberField.SUnit.sum_logEmbedding {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ↥((↑S).unit K)) :
      ∑ i : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } ⊕ ↥S, (logEmbedding S) (Additive.ofMul x) i = -↑NumberField.Units.dirichletUnitTheorem.w₀.mult * Real.log (NumberField.Units.dirichletUnitTheorem.w₀ ↑↑x)

      The sum of the S-logarithmic coordinates is the negative of the omitted infinite-place coordinate.

      source
      @[simp]
      theorem TauCeti.NumberField.SUnit.logEmbedding_unitOfUnits {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (u : (NumberField.RingOfIntegers K)ˣ) :
      (logEmbedding S) (Additive.ofMul ((SUnit.unitOfUnits (↑S) K) u)) = Sum.elim ((NumberField.Units.logEmbedding K) (Additive.ofMul u)) 0

      On ordinary units, the S-logarithmic embedding is the usual logarithmic embedding in the infinite coordinates and zero in the finite coordinates.