A normalized-factor product formula for the rational function field

This file proves the normalized-factor form of the degree-zero formula for a principal divisor on K(X). At every normalized prime factor, the multiplicity is identified with the actual Dedekind-domain exponent FractionalIdeal.count of the principal fractional ideal. Normalized polynomial factorization makes the finite contribution explicit; the remaining term is Mathlib's valuation at infinity. Packaging that finite contribution as one exhaustive sum over HeightOneSpectrum K[X] is completed in RatFuncExhaustiveProductFormula.

This is the base-field input for the Corvaja--Zannier valuation argument. It does not yet supply the corresponding formula for a finite extension of K(X): Mathlib currently has no packaged degree map on the divisor group of the integral closure, nor the global finite-place identity combining ramification and residue degrees over each base place.

noncomputable def BGS.CorvajaZannier.polynomialFinitePlace {K : Type u_1} [Field K] (r : Polynomial K) (hr : Prime r) : IsDedekindDomain.HeightOneSpectrum (Polynomial K)

The height-one prime of K[X] cut out by a prime polynomial.

Equations

• BGS.CorvajaZannier.polynomialFinitePlace r hr = { asIdeal := Ideal.span {r}, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem BGS.CorvajaZannier.polynomialFinitePlace_asIdeal {K : Type u_1} [Field K] (r : Polynomial K) (hr : Prime r) : (polynomialFinitePlace r hr).asIdeal = Ideal.span {r}

theorem BGS.CorvajaZannier.sum_normalizedFactor_natDegree {K : Type u_1} [Field K] [DecidableEq K] (p : Polynomial K) (hp : p ≠ 0) : ∑ r ∈ (UniqueFactorizationMonoid.normalizedFactors p).toFinset, Multiset.count r (UniqueFactorizationMonoid.normalizedFactors p) * r.natDegree = p.natDegree

The sum of the degrees of the normalized irreducible factors of a nonzero polynomial, with multiplicity, is its degree.

noncomputable def BGS.CorvajaZannier.ratFuncFiniteOrder {K : Type u_1} [Field K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) (f : RatFunc K) : ℤ

The additive order of a rational function at a finite polynomial place, implemented by the Dedekind-domain exponent of its principal fractional ideal.

Equations

• BGS.CorvajaZannier.ratFuncFiniteOrder v f = FractionalIdeal.count (RatFunc K) v ((FractionalIdeal.spanSingleton (nonZeroDivisors (Polynomial K))) f)

theorem BGS.CorvajaZannier.ratFuncFiniteOrder_polynomialFinitePlace {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (hf : f ≠ 0) (r : Polynomial K) (hr : Prime r) (hrnorm : normalize r = r) : ratFuncFiniteOrder (polynomialFinitePlace r hr) f = ↑(Multiset.count r (UniqueFactorizationMonoid.normalizedFactors f.num)) - ↑(Multiset.count r (UniqueFactorizationMonoid.normalizedFactors f.denom))

At a normalized prime polynomial, the Dedekind-domain order of a nonzero rational function is the numerator multiplicity minus the denominator multiplicity.

noncomputable def BGS.CorvajaZannier.ratFuncFinitePlaceDegreeSum {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) : ℤ

The degree-weighted finite-place contribution of a nonzero rational function, written as its zero contribution minus its pole contribution. The preceding theorem identifies the multiplicities here with FractionalIdeal.count at the corresponding height-one primes.

Equations

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

noncomputable def BGS.CorvajaZannier.ratFuncInfinityOrder {K : Type u_1} [Field K] (f : RatFunc K) : ℤ

The additive order at infinity. Mathlib's multiplicative infinity valuation sends a nonzero f to exp (-ratFuncInfinityOrder f).

Equations

• BGS.CorvajaZannier.ratFuncInfinityOrder f = -f.intDegree

theorem BGS.CorvajaZannier.inftyValuation_eq_exp_neg_ratFuncInfinityOrder {K : Type u_1} [Field K] [DecidableEq (RatFunc K)] (f : RatFunc K) (hf : f ≠ 0) : (RatFunc.inftyValuation K) f = WithZero.exp (-ratFuncInfinityOrder f)

theorem BGS.CorvajaZannier.ratFuncFinitePlaceDegreeSum_eq_intDegree {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (hf : f ≠ 0) : ratFuncFinitePlaceDegreeSum f = f.intDegree

theorem BGS.CorvajaZannier.ratFunc_finitePlace_plus_infinity_productFormula {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (hf : f ≠ 0) : ratFuncFinitePlaceDegreeSum f + ratFuncInfinityOrder f = 0

The normalized-factor form of the product formula for K(X): the degree-weighted numerator-minus-denominator contribution plus the order at infinity is zero.