The exhaustive finite-place product formula for the rational function field

This file packages the principal fractional ideal of a nonzero element of K(X) as a Finsupp on the full HeightOneSpectrum K[X]. Each height-one prime is identified with its canonical normalized prime-polynomial generator, so the degree-weighted sum can be reindexed to normalized polynomial factorization. The resulting exhaustive finite-place sum is f.intDegree; after adding Mathlib's order at infinity, the total is zero.

@[reducible, inline]

abbrev BGS.CorvajaZannier.NormalizedPrimePolynomial (K : Type u_2) [Field K] [DecidableEq K] : Type u_2

Normalized prime polynomials, i.e. the canonical polynomial representatives of finite places of K(X).

Equations

• BGS.CorvajaZannier.NormalizedPrimePolynomial K = { r : Polynomial K // Prime r ∧ normalize r = r }

noncomputable def BGS.CorvajaZannier.finitePlaceNormalizedPrime {K : Type u_1} [Field K] [DecidableEq K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : NormalizedPrimePolynomial K

The normalized prime polynomial generating a finite place of K(X).

Equations

• BGS.CorvajaZannier.finitePlaceNormalizedPrime v = ⟨normalize (Submodule.IsPrincipal.generator v.asIdeal), ⋯⟩

noncomputable def BGS.CorvajaZannier.normalizedPrimeFinitePlace {K : Type u_1} [Field K] [DecidableEq K] (r : NormalizedPrimePolynomial K) : IsDedekindDomain.HeightOneSpectrum (Polynomial K)

The finite place cut out by a normalized prime polynomial.

Equations

• BGS.CorvajaZannier.normalizedPrimeFinitePlace r = BGS.CorvajaZannier.polynomialFinitePlace ↑r ⋯

@[simp]

theorem BGS.CorvajaZannier.normalizedPrimeFinitePlace_finitePlaceNormalizedPrime {K : Type u_1} [Field K] [DecidableEq K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : normalizedPrimeFinitePlace (finitePlaceNormalizedPrime v) = v

@[simp]

theorem BGS.CorvajaZannier.finitePlaceNormalizedPrime_normalizedPrimeFinitePlace {K : Type u_1} [Field K] [DecidableEq K] (r : NormalizedPrimePolynomial K) : finitePlaceNormalizedPrime (normalizedPrimeFinitePlace r) = r

noncomputable def BGS.CorvajaZannier.normalizedPrimePolynomialEquivFinitePlace {K : Type u_1} [Field K] [DecidableEq K] : NormalizedPrimePolynomial K ≃ IsDedekindDomain.HeightOneSpectrum (Polynomial K)

Normalized prime polynomials are equivalent to all finite places of K(X).

Equations

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

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

The finitely supported principal divisor at all finite places.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.ratFuncFiniteDivisor_apply {K : Type u_1} [Field K] (f : RatFunc K) (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : (ratFuncFiniteDivisor f) v = ratFuncFiniteOrder v f

noncomputable def BGS.CorvajaZannier.ratFuncFinitePlaceDegree {K : Type u_1} [Field K] [DecidableEq K] (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ℕ

Degree of a finite place, defined using its canonical normalized prime generator.

Equations

• BGS.CorvajaZannier.ratFuncFinitePlaceDegree v = (↑(BGS.CorvajaZannier.finitePlaceNormalizedPrime v)).natDegree

@[simp]

theorem BGS.CorvajaZannier.ratFuncFinitePlaceDegree_normalizedPrimeFinitePlace {K : Type u_1} [Field K] [DecidableEq K] (r : NormalizedPrimePolynomial K) : ratFuncFinitePlaceDegree (normalizedPrimeFinitePlace r) = (↑r).natDegree

noncomputable def BGS.CorvajaZannier.normalizedPrimeFactorization {K : Type u_1} [Field K] [DecidableEq K] (p : Polynomial K) : NormalizedPrimePolynomial K →₀ ℕ

Factorization of a polynomial, restricted to normalized prime polynomials.

Equations

• BGS.CorvajaZannier.normalizedPrimeFactorization p = Finsupp.comapDomain Subtype.val (factorization p) ⋯

@[simp]

theorem BGS.CorvajaZannier.normalizedPrimeFactorization_apply {K : Type u_1} [Field K] [DecidableEq K] (p : Polynomial K) (r : NormalizedPrimePolynomial K) : (normalizedPrimeFactorization p) r = Multiset.count (↑r) (UniqueFactorizationMonoid.normalizedFactors p)

theorem BGS.CorvajaZannier.ratFuncFiniteOrder_eq_normalizedPrimeFactorization_sub {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (hf : f ≠ 0) (v : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ratFuncFiniteOrder v f = ↑((normalizedPrimeFactorization f.num) (finitePlaceNormalizedPrime v)) - ↑((normalizedPrimeFactorization f.denom) (finitePlaceNormalizedPrime v))

The coefficient of the finite principal divisor is the difference of the normalized-prime multiplicities in numerator and denominator.

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

The numerator-minus-denominator factorization on canonical normalized prime polynomial representatives.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.ratFuncNormalizedPrimeDivisor_apply {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (r : NormalizedPrimePolynomial K) : (ratFuncNormalizedPrimeDivisor f) r = ↑((normalizedPrimeFactorization f.num) r) - ↑((normalizedPrimeFactorization f.denom) r)

theorem BGS.CorvajaZannier.ratFuncFiniteDivisor_eq_equivMapDomain_normalizedPrimeDivisor {K : Type u_1} [Field K] [DecidableEq K] (f : RatFunc K) (hf : f ≠ 0) : ratFuncFiniteDivisor f = Finsupp.equivMapDomain normalizedPrimePolynomialEquivFinitePlace (ratFuncNormalizedPrimeDivisor f)

The count-defined finite principal divisor agrees with the transported normalized polynomial factorization.

theorem BGS.CorvajaZannier.normalizedPrimeFactorization_degreeSum {K : Type u_1} [Field K] [DecidableEq K] (p : Polynomial K) (hp : p ≠ 0) : ((normalizedPrimeFactorization p).sum fun (r : NormalizedPrimePolynomial K) (n : ℕ) => n * (↑r).natDegree) = p.natDegree

The degree-weighted factorization over canonical normalized prime representatives has total weight equal to polynomial degree.

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

The exhaustive degree-weighted sum over all height-one primes of K[X]. Its finite support is the support of the principal fractional ideal of f.

Equations

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

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

The actual exhaustive finite-place degree formula for K(X): the degree-weighted sum of the principal-divisor coefficients over every HeightOneSpectrum K[X] equals the rational-function degree.

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

The exhaustive finite-place sum plus the order at infinity is zero.