The global Wronskian divisor and the finite different degree

This module supplies two exact global pieces of the Corvaja--Zannier Wronskian argument for a finite separable extension of K(X).

First, a global derivation gives one global Wronskian element. Replacing it at a place by a local-parameter derivation changes the order by exactly the triangular multiple of the change-of-parameter coefficient. Accordingly, the local Wronskians form the sum of the principal divisor of the global Wronskian and a triangular multiple of a canonical correction divisor. The product formula then proves that its degree is exactly the triangular multiple of the canonical degree.

Second, for an integral primitive element in the finite integral closure, the weighted degree of the finite different is bounded by the degree of its power-basis discriminant. This is obtained without an abstract norm-of-ideal interface: ideal multiplicities are identified with finite-place orders, and the existing exhaustive norm formula evaluates their weighted sum.

What is deliberately not asserted here is a Riemann--Hurwitz theorem, an identification of the correction divisor at the places above infinity, or a plane-curve genus/boundary estimate. Those are the remaining geometric inputs needed to derive the final bound canonicalDegree + |S| <= 2ab.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.canonicalWronskianPolynomialAlgebra (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 canonical wronskian construction.

Equations

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

theorem BGS.CorvajaZannier.canonicalWronskianPolynomialScalarTower (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.canonicalWronskianFiniteIntegralClosureModuleFinite (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.canonicalWronskianPolynomialTorsionFreeTop (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.canonicalWronskianFiniteIntegralClosureIsIntegral (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.canonicalWronskianFiniteIntegralClosureIsTorsionFree (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)

The finite different and the discriminant degree

theorem BGS.CorvajaZannier.idealMultiplicityWeightedDegree_eq_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] (d : ↥(RatFuncFiniteIntegralClosure K L)) (hd : d ≠ 0) : ((idealMultiplicityDivisor (Ideal.span {d}) ⋯).sum fun (q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncFiniteIntegralClosure K L)) (e : ℕ) => ↑e * ↑(q.asIdeal.inertiaDeg (Polynomial K)) * ↑(ratFuncFinitePlaceDegree (IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q))) = finiteExtensionFiniteDirectDegreeSum K L ((algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) d)

The weighted degree of the principal ideal of an integral element is the finite-place degree sum of that element in the exhaustive K(X) model.

theorem BGS.CorvajaZannier.finiteDifferentDegree_le_minpolyDerivativeDegree (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 : ↥(RatFuncFiniteIntegralClosure K L)) (hx : (RatFunc K)[(algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) x] = ⊤) : ((differentMultiplicityDivisor (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ⋯).sum fun (q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncFiniteIntegralClosure K L)) (e : ℕ) => ↑e * ↑(q.asIdeal.inertiaDeg (Polynomial K)) * ↑(ratFuncFinitePlaceDegree (IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q))) ≤ finiteExtensionFiniteDirectDegreeSum K L ((algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) ((Polynomial.aeval x) (Polynomial.derivative (minpoly (Polynomial K) x))))

The finite different degree is bounded by the finite degree of the minimal-polynomial derivative of an integral primitive element.

theorem BGS.CorvajaZannier.finiteExtensionMinpolyDerivativeDegree_eq_powerBasisDiscriminantDegree (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 : ↥(RatFuncFiniteIntegralClosure K L)) (hx : (RatFunc K)[(algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) x] = ⊤) : finiteExtensionFiniteDirectDegreeSum K L ((algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) ((Polynomial.aeval x) (Polynomial.derivative (minpoly (Polynomial K) x)))) = (Algebra.discr (RatFunc K) ⇑(PowerBasis.ofAdjoinEqTop' ⋯ hx).basis).intDegree

The finite degree of the integral minimal-polynomial derivative is exactly the rational-function degree of the associated power-basis discriminant.

theorem BGS.CorvajaZannier.finiteDifferentDegree_le_powerBasisDiscriminantDegree (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 : ↥(RatFuncFiniteIntegralClosure K L)) (hx : (RatFunc K)[(algebraMap (↥(RatFuncFiniteIntegralClosure K L)) L) x] = ⊤) : ((differentMultiplicityDivisor (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L) ⋯).sum fun (q : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncFiniteIntegralClosure K L)) (e : ℕ) => ↑e * ↑(q.asIdeal.inertiaDeg (Polynomial K)) * ↑(ratFuncFinitePlaceDegree (IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q))) ≤ (Algebra.discr (RatFunc K) ⇑(PowerBasis.ofAdjoinEqTop' ⋯ hx).basis).intDegree

The finite different degree is bounded by the power-basis discriminant degree of any integral primitive element.

The local-parameter Wronskian divisor

def BGS.CorvajaZannier.finiteExtensionGlobalWronskian (L : Type u_2) [Field L] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (D : Derivation C L L) (g : Fin n → L) : L

The global ordinary Wronskian attached to one derivation.

Equations

• BGS.CorvajaZannier.finiteExtensionGlobalWronskian L D g = (BGS.Algebra.derivationWronskian D g).det

theorem BGS.CorvajaZannier.finitePlaceOrder_globalWronskian_changeParameter (L : Type u_2) [Field L] {C : Type u_3} [Field C] [Algebra C L] {R : Type u_4} [CommRing R] [IsDedekindDomain R] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) {n : ℕ} (D E : Derivation C L L) (a : L) (hD : D = a • E) (g : Fin n → L) (ha : a ≠ 0) (hE : finiteExtensionGlobalWronskian L E g ≠ 0) : finitePlaceOrder v (finiteExtensionGlobalWronskian L E g) = finitePlaceOrder v (finiteExtensionGlobalWronskian L D g) - ↑(n.choose 2) * finitePlaceOrder v a

Exact order change from a global derivation to a local-parameter derivation. If D = a E, then the local E-Wronskian has the global D-Wronskian order minus choose(n,2) times the order of a.

noncomputable def BGS.CorvajaZannier.finiteExtensionDivisorDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionPlace K L →₀ ℤ) : ℤ

Degree of a finitely supported divisor on the exhaustive places of the finite extension.

Equations

• BGS.CorvajaZannier.finiteExtensionDivisorDegree K L D = D.sum fun (v : BGS.CorvajaZannier.FiniteExtensionPlace K L) (e : ℤ) => e * ↑(BGS.CorvajaZannier.finiteExtensionPlaceDegree K L v)

noncomputable def BGS.CorvajaZannier.finiteExtensionLocalWronskianDivisor (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] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (D : Derivation C L L) (g : Fin n → L) (canonicalDivisor : FiniteExtensionPlace K L →₀ ℤ) : FiniteExtensionPlace K L →₀ ℤ

The divisor represented by local-parameter Wronskians: the principal divisor of the global Wronskian plus the triangular multiple of a supplied canonical correction divisor.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionLocalWronskianDivisor_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] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (D : Derivation C L L) (g : Fin n → L) (canonicalDivisor : FiniteExtensionPlace K L →₀ ℤ) (v : FiniteExtensionPlace K L) : (finiteExtensionLocalWronskianDivisor K L D g canonicalDivisor) v = ↑(n.choose 2) * canonicalDivisor v + (finiteExtensionPrincipalDivisor K L (finiteExtensionGlobalWronskian L D g)) v

theorem BGS.CorvajaZannier.finiteExtensionLocalWronskianDivisor_degree (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] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (D : Derivation C L L) (g : Fin n → L) (canonicalDivisor : FiniteExtensionPlace K L →₀ ℤ) (hW : finiteExtensionGlobalWronskian L D g ≠ 0) : finiteExtensionDivisorDegree K L (finiteExtensionLocalWronskianDivisor K L D g canonicalDivisor) = ↑(n.choose 2) * finiteExtensionDivisorDegree K L canonicalDivisor

The product formula kills the principal global Wronskian contribution. Thus the local Wronskian divisor has exactly the triangular multiple of the canonical degree.

theorem BGS.CorvajaZannier.finiteExtensionLocalWronskianDivisor_sum (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] {C : Type u_3} [Field C] [Algebra C L] [IsAlgClosed K] {n : ℕ} (D : Derivation C L L) (g : Fin n → L) (canonicalDivisor : FiniteExtensionPlace K L →₀ ℤ) (hW : finiteExtensionGlobalWronskian L D g ≠ 0) : ((finiteExtensionLocalWronskianDivisor K L D g canonicalDivisor).sum fun (x : FiniteExtensionPlace K L) (e : ℤ) => e) = ↑(n.choose 2) * canonicalDivisor.sum fun (x : FiniteExtensionPlace K L) (e : ℤ) => e

Over algebraically closed constants every place has degree one, so the global canonical identity becomes the ordinary unweighted sum of local Wronskian orders used by Corvaja--Zannier.

Final log-canonical arithmetic

theorem BGS.CorvajaZannier.canonicalDegree_add_boundaryCard_le_twice_bidegree {I : Type u_3} (S : Finset I) (canonicalDegree : ℤ) (firstDegree secondDegree : ℕ) (hCanonical : canonicalDegree + ↑(2 * (firstDegree + secondDegree)) ≤ ↑(2 * firstDegree * secondDegree)) (hBoundary : S.card ≤ 2 * (firstDegree + secondDegree)) : canonicalDegree + ↑S.card ≤ ↑(2 * firstDegree * secondDegree)

Once geometry bounds the canonical degree with the coarse boundary allowance 2(a+b), and the actual exceptional set has at most that many points, the exact Corvaja--Zannier choice chi = 2ab follows.

theorem BGS.CorvajaZannier.canonicalDegree_add_boundaryCard_le_twice_bidegree_of_genus_bound {I : Type u_3} (S : Finset I) (canonicalDegree : ℤ) (genus firstDegree secondDegree : ℕ) (hFirst : 0 < firstDegree) (hSecond : 0 < secondDegree) (hCanonical : canonicalDegree ≤ 2 * ↑genus - 2) (hGenus : genus ≤ (firstDegree - 1) * (secondDegree - 1)) (hBoundary : S.card ≤ 2 * (firstDegree + secondDegree)) : canonicalDegree + ↑S.card ≤ ↑(2 * firstDegree * secondDegree)

The usual genus and toric-boundary estimates imply the exact log-canonical allowance used by Corvaja--Zannier. This theorem is purely the numerical assembly: constructing a normalization and proving the two supplied geometric estimates remain separate obligations.

theorem BGS.CorvajaZannier.canonicalDegree_add_boundaryCard_le_twice_bidegree_of_different_bound {I : Type u_3} (S : Finset I) (canonicalDegree : ℤ) (totalDifferent firstDegree secondDegree : ℕ) (hSecond : 0 < secondDegree) (hCanonical : canonicalDegree ≤ ↑totalDifferent - 2 * ↑secondDegree) (hDifferent : totalDifferent ≤ (2 * secondDegree - 2) * firstDegree) (hBoundary : S.card ≤ 2 * (firstDegree + secondDegree)) : canonicalDegree + ↑S.card ≤ ↑(2 * firstDegree * secondDegree)

The divisor-theoretic replacement for the genus-bound assembly. If the canonical correction is bounded by the total different minus twice the projection degree, the sharp bivariate discriminant budget and the toric boundary budget give the same log-canonical bound 2 * a * b directly.