Finite places of the rational numbers

Every finite place of ℚ is exactly a p-adic absolute value, and every prime gives such a place. The equalities use Mathlib's Rat.HeightOneSpectrum.primesEquiv to identify the prime of a place and preserve normalization, not just equivalence of absolute values. This is needed to translate products over finite places into the products of padicNorm occurring in Ridout's theorem.

Ostrowski's theorem supplies equivalence with a p-adic absolute value. The known value at the rational prime generating the place's maximal ideal then fixes the prime and exponent. The inverse dictionary uses primesEquiv.symm to supply the corresponding finite place. The local-value formulas Rat.HeightOneSpectrum.finitePlace_mk_natGenerator and Rat.HeightOneSpectrum.finitePlace_mk_inv_natGenerator evaluate a place at its generating prime and its inverse.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, §6.2.
• The original height-based normalization argument followed Ralf Stephan's DiophantineApproximation/RationalPlaces.lean in rwst/Subspace-Theorems, revision 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0). Here the existing local-value formulas replace that height computation.

theorem Rat.HeightOneSpectrum.finitePlace_mk_natGenerator (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) : (NumberField.FinitePlace.mk v) ↑(natGenerator v) = (↑(natGenerator v))⁻¹

The absolute value of the rational prime of v at the finite place v is its inverse.

theorem Rat.HeightOneSpectrum.finitePlace_mk_inv_natGenerator (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) : (NumberField.FinitePlace.mk v) (↑(natGenerator v))⁻¹ = ↑(natGenerator v)

The absolute value of the inverse of the rational prime of v at the finite place v is the prime.

theorem NumberField.FinitePlace.val_eq_padic (v : FinitePlace ℚ) : ↑v = Rat.AbsoluteValue.padic ↑(Rat.HeightOneSpectrum.primesEquiv v.maximalIdeal)

A finite place of ℚ is the usual p-adic absolute value at its canonical prime under Rat.HeightOneSpectrum.primesEquiv, not merely a positive power of that absolute value.

theorem NumberField.FinitePlace.apply_eq_padicNorm (v : FinitePlace ℚ) (x : ℚ) : v x = ↑(padicNorm (↑(Rat.HeightOneSpectrum.primesEquiv v.maximalIdeal)) x)

A finite place of ℚ, evaluated at a rational number, is padicNorm at its canonical prime under Rat.HeightOneSpectrum.primesEquiv.

theorem Nat.Primes.finitePlace_mk_val_eq_padic (p : Primes) : ↑(NumberField.FinitePlace.mk (Rat.HeightOneSpectrum.primesEquiv.symm p)) = Rat.AbsoluteValue.padic ↑p

The finite place corresponding to a prime under Rat.HeightOneSpectrum.primesEquiv.symm has exactly the usual p-adic absolute value.

theorem Nat.Primes.finitePlace_mk_apply (p : Primes) (x : ℚ) : (NumberField.FinitePlace.mk (Rat.HeightOneSpectrum.primesEquiv.symm p)) x = ↑(padicNorm (↑p) x)

The finite place constructed from a prime evaluates to the usual padicNorm.