Weak approximation at finite places

This file proves the finite-place weak-approximation theorem needed for function-field Riemann--Roch constructions. For finitely many distinct height-one prime ideals, one may prescribe an element of the fraction field to arbitrary positive order. The resulting global fraction is integral at every other height-one prime.

The proof is elementary Dedekind-domain algebra. First clear all prescribed fractions by one denominator. The numerator is then chosen by the Chinese remainder theorem. At a selected prime the modulus contains both the desired precision and the multiplicity of the common denominator. At every other prime dividing the denominator, a zero residue cancels the complete denominator multiplicity.

Mathlib's multiplicative adic valuation is exp (-order). Thus v.valuation L (z - x) ≤ exp (-n) means that z - x has additive order at least n, while v.valuation L z ≤ 1 means that z is regular at v.

theorem BGS.HasseWeil.valuation_div_algebraMap_le_one_of_mem_denominatorPower {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (numerator denominator : R) (hdenominator : denominator ≠ 0) (hnumerator : numerator ∈ v.asIdeal ^ Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {denominator}))) : (IsDedekindDomain.HeightOneSpectrum.valuation L v) ((algebraMap R L) numerator / (algebraMap R L) denominator) ≤ 1

If the numerator contains every occurrence of a height-one prime in the denominator, the resulting fraction is integral at that prime.

theorem BGS.HasseWeil.valuation_sub_div_algebraMap_le_of_mem_denominatorPrecisionPower {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (numerator target denominator : R) (precision : ℕ) (hdenominator : denominator ≠ 0) (hnumerator : numerator - target ∈ v.asIdeal ^ (precision + Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {denominator})))) : (IsDedekindDomain.HeightOneSpectrum.valuation L v) ((algebraMap R L) numerator / (algebraMap R L) denominator - (algebraMap R L) target / (algebraMap R L) denominator) ≤ WithZero.exp (-↑precision)

A congruence modulo the desired prime power plus the denominator multiplicity gives the corresponding adic approximation bound after division by the denominator.

theorem BGS.HasseWeil.exists_numerator_prescribedPrimePower_and_denominatorSupport {R : Type u_1} [CommRing R] [IsDedekindDomain R] (selected : Finset (Ideal R)) (denominatorIdeal : Ideal R) (hselectedPrime : ∀ P ∈ selected, Prime P) (target : ↥selected → R) (precision : ↥selected → ℕ) : ∃ (numerator : R), (∀ (P : ↥selected), numerator - target P ∈ ↑P ^ (precision P + Multiset.count (↑P) (UniqueFactorizationMonoid.normalizedFactors denominatorIdeal))) ∧ ∀ Q ∈ (UniqueFactorizationMonoid.normalizedFactors denominatorIdeal).toFinset, Q ∉ selected → numerator ∈ Q ^ Multiset.count Q (UniqueFactorizationMonoid.normalizedFactors denominatorIdeal)

Chinese-remainder numerator selection with simultaneous denominator cancellation. At selected primes the congruence precision is increased by the denominator multiplicity. Every unselected prime factor of the denominator divides the chosen numerator to its full multiplicity.

theorem BGS.HasseWeil.exists_fraction_approximating_at_finitePlaces_regular_elsewhere {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (selected : Finset (Ideal R)) (hselectedPrime : ∀ P ∈ selected, Prime P) (target : Ideal R → L) (precision : Ideal R → ℕ) : ∃ (z : L), (∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ∈ selected → (IsDedekindDomain.HeightOneSpectrum.valuation L v) (z - target v.asIdeal) ≤ WithZero.exp (-↑(precision v.asIdeal))) ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.asIdeal ∉ selected → (IsDedekindDomain.HeightOneSpectrum.valuation L v) z ≤ 1

Finite-place weak approximation in a Dedekind fraction field.

The selected ideals must be prime. The function target prescribes a local fraction at each selected ideal, and precision prescribes its approximation order. The returned global fraction has that approximation order at every selected height-one place and is integral at every unselected height-one place.