Heights of S-integers

The height of an S-integer is supported on the primes in S and the infinite places. This file translates membership in Mathlib's S-integers and S-units into finite-place absolute values, proves the resulting multiplicative and logarithmic height identities, shows that the multiplicative identity characterizes S-integers, and records the product formula for an S-unit as a product over the infinite places and S (NumberField.prod_abs_eq_one_of_mem_unit). The set S may be arbitrary; finset versions give ordinary products and sums. At S = ∅ the element 1 / 2 shows that the S-integer hypothesis cannot be dropped.

Adapted from Ralf Stephan's ArithmeticHeights/SUnit.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0), using Mathlib's height API. The mathematical reference is Bombieri and Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.5.10.

theorem Set.mem_integer_iff_finitePlace {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : K) : x ∈ S.integer K ↔ ∀ v ∉ S, (NumberField.FinitePlace.mk v) x ≤ 1

An S-integer is an element whose absolute values at the finite places outside S are at most 1.

theorem Set.mem_unit_iff_finitePlace {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : Kˣ) : x ∈ S.unit K ↔ ∀ v ∉ S, (NumberField.FinitePlace.mk v) ↑x = 1

An S-unit is an element of Kˣ whose absolute values at the finite places outside S are all 1.

theorem NumberField.exists_sUnit_coe_eq {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {x : K} (hx0 : x ≠ 0) (hx : ∀ v ∉ S, (HeightOneSpectrum.adicAbv K v) x = 1) : ∃ (y : ↥(S.unit K)), ↑↑y = x

A nonzero element of K which has absolute value 1 at every finite place outside S is an S-unit.

theorem NumberField.mulHeight₁_eq_of_mem_integer {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : K} (hx : x ∈ S.integer K) : Height.mulHeight₁ x = (∏ w : InfinitePlace K, max (w x) 1 ^ w.mult) * ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (_ : v ∈ S), max ((FinitePlace.mk v) x) 1

The height of an S-integer is carried by the infinite places and the places of S. The S-unit case of this is Bombieri–Gubler 1.5.10; the hypothesis the proof uses is only that x is an S-integer.

theorem NumberField.logHeight₁_eq_of_mem_integer {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : K} (hx : x ∈ S.integer K) : Height.logHeight₁ x = ∑ w : InfinitePlace K, ↑w.mult * (w x).posLog + ∑ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (_ : v ∈ S), ((FinitePlace.mk v) x).posLog

The logarithmic form of NumberField.mulHeight₁_eq_of_mem_integer.

theorem NumberField.mulHeight₁_eq_of_mem_unit {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : Kˣ} (hx : x ∈ S.unit K) : Height.mulHeight₁ ↑x = (∏ w : InfinitePlace K, max (w ↑x) 1 ^ w.mult) * ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (_ : v ∈ S), max ((FinitePlace.mk v) ↑x) 1

The height of an S-unit, the statement of Bombieri–Gubler 1.5.10.

theorem NumberField.logHeight₁_eq_of_mem_unit {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : Kˣ} (hx : x ∈ S.unit K) : Height.logHeight₁ ↑x = ∑ w : InfinitePlace K, ↑w.mult * (w ↑x).posLog + ∑ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (_ : v ∈ S), ((FinitePlace.mk v) ↑x).posLog

The logarithmic form of NumberField.mulHeight₁_eq_of_mem_unit.

theorem NumberField.mulHeight₁_eq_prod_of_mem_integer {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : K} (hx : x ∈ (↑S).integer K) : Height.mulHeight₁ x = (∏ w : InfinitePlace K, max (w x) 1 ^ w.mult) * ∏ v ∈ S, max ((FinitePlace.mk v) x) 1

The height of an S-integer when S is a finite set of primes.

theorem NumberField.logHeight₁_eq_sum_of_mem_integer {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : K} (hx : x ∈ (↑S).integer K) : Height.logHeight₁ x = ∑ w : InfinitePlace K, ↑w.mult * (w x).posLog + ∑ v ∈ S, ((FinitePlace.mk v) x).posLog

The logarithmic height of an S-integer when S is a finite set of primes.

theorem NumberField.prod_abs_eq_one_of_mem_unit {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {u : Kˣ} (hu : u ∈ (↑S).unit K) : (∏ w : InfinitePlace K, w ↑u ^ w.mult) * ∏ v ∈ S, (FinitePlace.mk v) ↑u = 1

The product formula for an S-unit: its absolute values at the infinite places, with multiplicities, and at the places of S multiply to 1. This is Mathlib's prod_abs_eq_one with the factors at the finite places outside S, all equal to 1, removed.

The identity characterizes the S-integers

theorem NumberField.mulHeight₁_eq_iff_mem_integer {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) {x : K} : Height.mulHeight₁ x = (∏ w : InfinitePlace K, max (w x) 1 ^ w.mult) * ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (_ : v ∈ S), max ((FinitePlace.mk v) x) 1 ↔ x ∈ S.integer K

The display of NumberField.mulHeight₁_eq_of_mem_integer characterizes the S-integers. Every local factor is at least 1, so a finite place outside S at which x has absolute value greater than 1 makes the full finite product strictly larger than its part over S.

The S-integer hypothesis cannot be dropped

At S = ∅ the identity says that the height of an algebraic integer is carried by the infinite places. The element 1 / 2 is not an algebraic integer: its infinite factor is 1, while its height is 2 ^ [K : ℚ], all of it carried by the finite places above 2.