Principal divisors on the exhaustive places of a finite function field

This file packages the finite primes and the primes above infinity of a finite separable extension L / K(X) into one place type. Principal divisors on that type have finite support. Their degree-weighted sum is proved to vanish by regrouping finite primes below K[X] and applying the exhaustive norm product formula.

It also provides common finite supports for arbitrary finite families, degree-weighted product formulas on those family place types, and the positive degree / pole-height decomposition. Over an algebraically closed constant field, all finite and above-infinity residue degrees are proved equal to one, so the ordinary-order specialization has no residual place-degree hypothesis.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.principalDivisorPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension principal divisor construction.

Equations

• BGS.CorvajaZannier.principalDivisorPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.principalDivisorPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.CorvajaZannier.principalDivisorFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorPolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.CorvajaZannier.principalDivisorFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorInfinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorInfinityIntegralClosureIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.principalDivisorInfinityIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

noncomputable def BGS.CorvajaZannier.finitePlaceFiberEquivPrimesOver (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : { q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncFiniteIntegralClosure K L) // IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q = p } ≃ ↑(p.asIdeal.primesOver ↥(RatFuncFiniteIntegralClosure K L))

Finite places over a base place correspond to prime ideals lying above its ideal.

Equations

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

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionFinitePlace (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Type u_2

Finite places of the extension, represented by height-one primes of its finite integral closure.

Equations

• BGS.CorvajaZannier.FiniteExtensionFinitePlace K L = IsDedekindDomain.HeightOneSpectrum ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionInfinityPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Set (Ideal ↥(RatFuncInfinityIntegralClosure K L))

Infinity places of the extension, represented by primes over the base infinity place.

Equations

• BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L = (BGS.CorvajaZannier.ratFuncInfinityPlace K).asIdeal.primesOver ↥(BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K L)

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Type u_2

The disjoint union of finite and infinity places of the extension.

Equations

• BGS.CorvajaZannier.FiniteExtensionPlace K L = (BGS.CorvajaZannier.FiniteExtensionFinitePlace K L ⊕ ↑(BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L))

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.principalDivisorInfinityPlaceFintype (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Fintype ↑(FiniteExtensionInfinityPlace K L)

A finite enumeration of (FiniteExtensionInfinityPlace K L) used in the finite extension principal divisor construction.

Equations

• BGS.CorvajaZannier.principalDivisorInfinityPlaceFintype K L = ⋯.fintype

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePrincipalDivisor (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : FiniteExtensionFinitePlace K L →₀ ℤ

The finite-place part of the principal divisor of an extension-field element.

Equations

• BGS.CorvajaZannier.finiteExtensionFinitePrincipalDivisor K L x = BGS.CorvajaZannier.finitePrincipalDivisor ((BGS.CorvajaZannier.ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFinitePrincipalDivisor_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionFinitePrincipalDivisor K L x) q = finitePlaceOrder q ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityPrincipalDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ↑(FiniteExtensionInfinityPlace K L) →₀ ℤ

The infinity-place part of the principal divisor of an extension-field element.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionInfinityPrincipalDivisor_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (P : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionInfinityPrincipalDivisor K L x) P = finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) ((ratFuncInfinityIntegralClosureFractionRingEquiv K L).symm x)

noncomputable def BGS.CorvajaZannier.finiteExtensionPrincipalDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : FiniteExtensionPlace K L →₀ ℤ

The principal divisor on all finite and infinity places of the extension.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_inl (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionPrincipalDivisor K L x) (Sum.inl q) = finitePlaceOrder q ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_inr (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (P : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionPrincipalDivisor K L x) (Sum.inr P) = finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) ((ratFuncInfinityIntegralClosureFractionRingEquiv K L).symm x)

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteResidueWeightedDivisor (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : FiniteExtensionFinitePlace K L →₀ ℤ

The finite-place principal divisor weighted by residue degrees.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFiniteResidueWeightedDivisor_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionFiniteResidueWeightedDivisor K L x) q = ↑(q.asIdeal.inertiaDeg (Polynomial K)) * finitePlaceOrder q ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDivisorBelow (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : IsDedekindDomain.HeightOneSpectrum (Polynomial K) →₀ ℤ

The finite-place principal divisor pushed down to base places with residue-degree weights.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionFiniteDivisorBelow_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : (finiteExtensionFiniteDivisorBelow K L x) p = ∑ P : ↑(p.asIdeal.primesOver ↥(RatFuncFiniteIntegralClosure K L)), ↑((↑P).inertiaDeg (Polynomial K)) * finitePlaceOrder (primeOverHeightOne p P) ((ratFuncFiniteIntegralClosureFractionRingEquiv K L).symm x)

theorem BGS.CorvajaZannier.finiteExtensionFiniteDivisorBelow_eq_normDivisor (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionFiniteDivisorBelow K L x = ratFuncFiniteDivisor ((Algebra.norm (RatFunc K)) x)

noncomputable def BGS.CorvajaZannier.finiteExtensionFiniteDirectDegreeSum (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℤ

The finite-place degree sum written directly on the height-one primes of the finite integral closure.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionFiniteDirectDegreeSum_eq_grouped (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionFiniteDirectDegreeSum K L x = finiteExtensionFinitePlaceDegreeSum K L x

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityDirectDegreeSum (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℤ

The above-infinity order sum written as a Finsupp.sum on the infinity part of the principal divisor.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionInfinityDirectDegreeSum_eq_grouped (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : finiteExtensionInfinityDirectDegreeSum K L x = finiteExtensionInfinityOrderSum K L x

noncomputable def BGS.CorvajaZannier.finiteExtensionPlaceDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FiniteExtensionPlace K L → ℕ

Degree of a place of L: residue degree times the degree of the place below it. The place at infinity of K(X) has degree one.

Equations

• One or more equations did not get rendered due to their size.
• BGS.CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P) = (↑P).inertiaDeg ↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)

noncomputable def BGS.CorvajaZannier.finiteExtensionPrincipalDivisorDegreeSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℤ

Degree of the exhaustive principal divisor, summed on the actual finite and above-infinity places of L.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisorDegreeSum_eq_grouped (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionPrincipalDivisorDegreeSum K L x = finiteExtensionFinitePlaceDegreeSum K L x + finiteExtensionInfinityOrderSum K L x

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisorDegreeSum_eq_zero (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionPrincipalDivisorDegreeSum K L x = 0

Product formula on the actual place type, rather than grouped below the base places.

noncomputable def BGS.CorvajaZannier.finiteExtensionPositiveDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℕ

Positive degree of the principal divisor of x.

Equations

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

noncomputable def BGS.CorvajaZannier.finiteExtensionHeight (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ℕ

Pole height of x, i.e. the degree of the negative part of its principal divisor.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_cast (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ↑(finiteExtensionPositiveDegree K L x) = ∑ v ∈ (finiteExtensionPrincipalDivisor K L x).support with 0 < (finiteExtensionPrincipalDivisor K L x) v, (finiteExtensionPrincipalDivisor K L x) v * ↑(finiteExtensionPlaceDegree K L v)

theorem BGS.CorvajaZannier.finiteExtensionHeight_negativeSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : -↑(finiteExtensionHeight K L x) = ∑ v ∈ (finiteExtensionPrincipalDivisor K L x).support with (finiteExtensionPrincipalDivisor K L x) v < 0, (finiteExtensionPrincipalDivisor K L x) v * ↑(finiteExtensionPlaceDegree K L v)

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_eq_height (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionPositiveDegree K L x = finiteExtensionHeight K L x

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.familyPlaceDecidableEq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : DecidableEq (FiniteExtensionPlace K L)

Decidable equality on (FiniteExtensionPlace K L) used in the finite extension principal divisor construction.

Equations

• BGS.CorvajaZannier.familyPlaceDecidableEq K L = Classical.decEq (BGS.CorvajaZannier.FiniteExtensionPlace K L)

noncomputable def BGS.CorvajaZannier.finiteExtensionFamilySupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) : Finset (FiniteExtensionPlace K L)

A single finite place set supporting the principal divisors of every member of a finite family.

Equations

• BGS.CorvajaZannier.finiteExtensionFamilySupport K L f = Finset.univ.biUnion fun (a : A) => (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L (f a)).support

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionFamilyPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) : Type u_2

A finite or infinity place appearing in the principal divisor of a member of a family.

Equations

• BGS.CorvajaZannier.FiniteExtensionFamilyPlace K L f = ↥(BGS.CorvajaZannier.finiteExtensionFamilySupport K L f)

noncomputable def BGS.CorvajaZannier.finiteExtensionFamilyOrder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (v : FiniteExtensionFamilyPlace K L f) : ℤ

Ordinary order of a family member on the common finite place set.

Equations

• BGS.CorvajaZannier.finiteExtensionFamilyOrder K L f a v = (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L (f a)) ↑v

noncomputable def BGS.CorvajaZannier.finiteExtensionFamilyWeightedOrder (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (v : FiniteExtensionFamilyPlace K L f) : ℤ

Degree-weighted order. These are the values whose unweighted sum is zero without any algebraic-closedness assumption on the constant field.

Equations

• BGS.CorvajaZannier.finiteExtensionFamilyWeightedOrder K L f a v = BGS.CorvajaZannier.finiteExtensionFamilyOrder K L f a v * ↑(BGS.CorvajaZannier.finiteExtensionPlaceDegree K L ↑v)

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_support_subset_familySupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : (finiteExtensionPrincipalDivisor K L (f a)).support ⊆ finiteExtensionFamilySupport K L f

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_eq_zero_of_not_mem_support (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (v : FiniteExtensionFamilyPlace K L f) (hv : ↑v ∉ (finiteExtensionPrincipalDivisor K L (f a)).support) : finiteExtensionFamilyOrder K L f a v = 0

theorem BGS.CorvajaZannier.finiteExtensionFamilyWeightedOrder_sum_eq_zero (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (ha : f a ≠ 0) : ∑ v : FiniteExtensionFamilyPlace K L f, finiteExtensionFamilyWeightedOrder K L f a v = 0

Product formula for any member of an arbitrary finite family, on the one common finite place type attached to that family.

theorem BGS.CorvajaZannier.finiteExtensionFamilyWeightedPositiveSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : ∑ v : FiniteExtensionFamilyPlace K L f with 0 < finiteExtensionFamilyOrder K L f a v, finiteExtensionFamilyWeightedOrder K L f a v = ↑(finiteExtensionPositiveDegree K L (f a))

theorem BGS.CorvajaZannier.finiteExtensionFamilyWeightedNegativeSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : ∑ v : FiniteExtensionFamilyPlace K L f with finiteExtensionFamilyOrder K L f a v < 0, finiteExtensionFamilyWeightedOrder K L f a v = -↑(finiteExtensionHeight K L (f a))

noncomputable def BGS.CorvajaZannier.finiteExtensionFamilyOutsideHeight (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (S : Finset (FiniteExtensionFamilyPlace K L f)) (a : A) : ℕ

Pole height outside a caller-specified exceptional set. This is the quantity occurring on the right of the global Wronskian inequality.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionFamilyOutsideHeight_negativeSum (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (S : Finset (FiniteExtensionFamilyPlace K L f)) (a : A) : ∑ v : FiniteExtensionFamilyPlace K L f with v ∉ S ∧ finiteExtensionFamilyOrder K L f a v < 0, finiteExtensionFamilyWeightedOrder K L f a v = -↑(finiteExtensionFamilyOutsideHeight K L f S a)

theorem BGS.CorvajaZannier.globalWronskianInequality_of_finiteExtensionWeightedPlacewiseBounds (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV iRho iGrid iW : A) (S : Finset (FiniteExtensionFamilyPlace K L f)) (h k n sigma chi : ℕ) (canonicalDegree : ℤ) (hUne : f iU ≠ 0) (hGridne : f iGrid ≠ 0) (hUOutside : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iU i = 0) (hGridOutside : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iGrid i = 0) (hVPositiveSupport : ∀ (i : FiniteExtensionFamilyPlace K L f), 0 < finiteExtensionFamilyOrder K L f iV i → i ∈ S) (hCanonical : ∑ i : FiniteExtensionFamilyPlace K L f, finiteExtensionFamilyWeightedOrder K L f iW i = ↑sigma * canonicalDegree) (hEuler : canonicalDegree + ↑(∑ i ∈ S, finiteExtensionPlaceDegree K L ↑i) ≤ ↑chi) (hRhoSupport : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ i ∈ S, finiteExtensionFamilyWeightedOrder K L f iRho i) (hCaseI : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iRho i < 0 → ↑n * finiteExtensionFamilyOrder K L f iRho i ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseII : ∀ i ∉ S, 0 ≤ finiteExtensionFamilyOrder K L f iRho i → 0 ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseIII : ∀ i ∈ S, 0 < finiteExtensionFamilyOrder K L f iV i → ↑(k * (k - 1) / 2) * finiteExtensionFamilyOrder K L f iU i + ↑(h * k) * finiteExtensionFamilyOrder K L f iV i + ↑k * finiteExtensionFamilyOrder K L f iRho i + finiteExtensionFamilyOrder K L f iGrid i - ↑sigma ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseIV : ∀ i ∈ S, finiteExtensionFamilyOrder K L f iV i ≤ 0 → ↑(k * (k - 1) / 2) * finiteExtensionFamilyOrder K L f iU i + ↑k * finiteExtensionFamilyOrder K L f iRho i + finiteExtensionFamilyOrder K L f iGrid i - ↑sigma ≤ finiteExtensionFamilyOrder K L f iW i) : ↑(h * k) * ↑(finiteExtensionPositiveDegree K L (f iV)) - ↑k * (↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) - ↑sigma * ↑chi ≤ ↑n * ↑(finiteExtensionFamilyOutsideHeight K L f S iRho)

The residue-degree-weighted Corvaja--Zannier summation on the exhaustive family place type. Unlike the later degree-one specialization, this theorem does not assume that the constant field is algebraically closed.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.finiteIntegralClosureConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension principal divisor construction.

Equations

• BGS.CorvajaZannier.finiteIntegralClosureConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.CorvajaZannier.finiteIntegralClosureConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

noncomputable def BGS.CorvajaZannier.ratFuncFinitePlaceResidueEquiv (K : Type u_1) [Field K] [DecidableEq K] [IsAlgClosed K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : p.asIdeal.ResidueField ≃ₐ[K] K

The residue-field equivalence at a finite place of the rational function field.

Equations

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

theorem BGS.CorvajaZannier.ratFuncFinitePlaceDegree_eq_one (K : Type u_1) [Field K] [DecidableEq K] [IsAlgClosed K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ratFuncFinitePlaceDegree p = 1

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_inertiaDeg_eq_one (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] (q : FiniteExtensionFinitePlace K L) : q.asIdeal.inertiaDeg (Polynomial K) = 1

theorem BGS.CorvajaZannier.finiteExtensionPlaceDegree_eq_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] (v : FiniteExtensionPlace K L) : finiteExtensionPlaceDegree K L v = 1

Over an algebraically closed constant field, all actual places of the extension have degree one.

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_sum_eq_zero (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (ha : f a ≠ 0) : ∑ v : FiniteExtensionFamilyPlace K L f, finiteExtensionFamilyOrder K L f a v = 0

Ordinary (unweighted) product formula on the common family place type.

theorem BGS.CorvajaZannier.finiteExtensionFamilyWeightedOrder_eq_order (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (v : FiniteExtensionFamilyPlace K L f) : finiteExtensionFamilyWeightedOrder K L f a v = finiteExtensionFamilyOrder K L f a v

theorem BGS.CorvajaZannier.globalWronskianInequality_of_finiteExtensionPlacewiseBounds (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [IsAlgClosed K] {A : Type u_3} [Fintype A] (f : A → L) (iU iV iRho iGrid iW : A) (S : Finset (FiniteExtensionFamilyPlace K L f)) (h k n sigma chi : ℕ) (canonicalDegree : ℤ) (hUne : f iU ≠ 0) (hGridne : f iGrid ≠ 0) (hUOutside : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iU i = 0) (hGridOutside : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iGrid i = 0) (hVPositiveSupport : ∀ (i : FiniteExtensionFamilyPlace K L f), 0 < finiteExtensionFamilyOrder K L f iV i → i ∈ S) (hCanonical : ∑ i : FiniteExtensionFamilyPlace K L f, finiteExtensionFamilyOrder K L f iW i = ↑sigma * canonicalDegree) (hEuler : canonicalDegree + ↑S.card ≤ ↑chi) (hRhoSupport : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ i ∈ S, finiteExtensionFamilyOrder K L f iRho i) (hCaseI : ∀ i ∉ S, finiteExtensionFamilyOrder K L f iRho i < 0 → ↑n * finiteExtensionFamilyOrder K L f iRho i ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseII : ∀ i ∉ S, 0 ≤ finiteExtensionFamilyOrder K L f iRho i → 0 ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseIII : ∀ i ∈ S, 0 < finiteExtensionFamilyOrder K L f iV i → ↑(k * (k - 1) / 2) * finiteExtensionFamilyOrder K L f iU i + ↑(h * k) * finiteExtensionFamilyOrder K L f iV i + ↑k * finiteExtensionFamilyOrder K L f iRho i + finiteExtensionFamilyOrder K L f iGrid i - ↑sigma ≤ finiteExtensionFamilyOrder K L f iW i) (hCaseIV : ∀ i ∈ S, finiteExtensionFamilyOrder K L f iV i ≤ 0 → ↑(k * (k - 1) / 2) * finiteExtensionFamilyOrder K L f iU i + ↑k * finiteExtensionFamilyOrder K L f iRho i + finiteExtensionFamilyOrder K L f iGrid i - ↑sigma ≤ finiteExtensionFamilyOrder K L f iW i) : ↑(h * k) * ↑(finiteExtensionPositiveDegree K L (f iV)) - ↑k * (↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) - ↑sigma * ↑chi ≤ ↑n * ↑(finiteExtensionFamilyOutsideHeight K L f S iRho)

The global Corvaja--Zannier summation specialized to the exhaustive family place type. Principal-divisor sums, the positive degree of V, and the pole height of rho outside S are discharged by this file. The exceptional-set support conditions, canonical-divisor identity and bound, rho support bound, and the four local Wronskian estimates remain explicit inputs.