Finite places and their adic completions

Let R be a Dedekind domain with fraction field L. Mathlib supplies both the exponent FractionalIdeal.count L v I of a height-one prime v in a fractional ideal I and the v-adic completion of L. This file connects those two interfaces for principal fractional ideals.

For a nonzero global function x, the valuation of its image in the actual adic completion is exp (-ord_v(x)), where ord_v(x) is the exponent of v in (x). The orders at all finite places are also packaged as a genuine finitely supported divisor. This is the finite-place part of the global divisor infrastructure needed in the Corvaja--Zannier Wronskian argument.

It does not add the places above infinity, a degree map on divisors, or the canonical-divisor degree formula.

noncomputable def BGS.CorvajaZannier.finitePlaceOrder {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : ℤ

The additive order of x at the finite place v, defined as the exponent of v in the principal fractional ideal (x).

Equations

• BGS.CorvajaZannier.finitePlaceOrder v x = FractionalIdeal.count L v ((FractionalIdeal.spanSingleton (nonZeroDivisors R)) x)

theorem BGS.CorvajaZannier.valuation_eq_exp_neg_finitePlaceOrder {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) (hx : x ≠ 0) : (IsDedekindDomain.HeightOneSpectrum.valuation L v) x = WithZero.exp (-finitePlaceOrder v x)

The multiplicative v-adic valuation is the exponential of minus the additive order defined by principal fractional-ideal factorization.

noncomputable def BGS.CorvajaZannier.finitePlaceCompletionEmbedding {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) : L →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion L v

The canonical embedding of the global fraction field into the actual adic completion attached to a finite place.

Equations

• BGS.CorvajaZannier.finitePlaceCompletionEmbedding v = algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L v)

theorem BGS.CorvajaZannier.finitePlaceCompletionEmbedding_injective {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) : Function.Injective ⇑(finitePlaceCompletionEmbedding v)

theorem BGS.CorvajaZannier.valued_finitePlaceCompletionEmbedding_eq_exp_neg_order {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) (hx : x ≠ 0) : Valued.v ((finitePlaceCompletionEmbedding v) x) = WithZero.exp (-finitePlaceOrder v x)

After the canonical completion embedding, the completed-field valuation still records the exponent of v in the global principal fractional ideal.

noncomputable def BGS.CorvajaZannier.finitePrincipalDivisor {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (x : L) : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ

The finite-place part of the principal divisor of x. Finiteness is provided by unique factorization of nonzero fractional ideals in a Dedekind domain (and is harmlessly true for x = 0 under Mathlib's count 0 = 0 convention).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.CorvajaZannier.finitePrincipalDivisor_apply {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (x : L) (v : IsDedekindDomain.HeightOneSpectrum R) : (finitePrincipalDivisor x) v = finitePlaceOrder v x

theorem BGS.CorvajaZannier.finitePrincipalDivisor_mul {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finitePrincipalDivisor (x * y) = finitePrincipalDivisor x + finitePrincipalDivisor y

The finite principal divisor of a nonzero product is the sum of the two finite principal divisors.