Global canonical bound from a normalized derivation

The finite-place branch is now completely automatic: the different supplies the canonical clearing scalar, and the four local estimates are selected after splitting the exhaustive place type. This module leaves only the four corresponding infinity statements as explicit inputs.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.globalNormalizedPolynomialAlgebra (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 global normalized construction.

Equations

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

theorem BGS.CorvajaZannier.globalNormalizedPolynomialScalarTower (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.globalNormalizedFiniteIntegralClosureModuleFinite (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.globalNormalizedFiniteIntegralClosureIsIntegral (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.globalNormalizedPolynomialTorsionFreeTop (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.globalNormalizedFiniteIntegralClosureIsTorsionFree (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.finiteExtensionGcdBound_of_normalizedCanonicalInfinityPlacewiseBounds (K : Type u_1) [Field K] [Finite 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] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) (h k : ℕ) (hn : 0 < h * k + h + k) (chi : ℕ) (hWronskian : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) (hEuler : finiteExtensionDivisorDegree K L (finiteExtensionCanonicalDifferentDivisor K L ⋯) + ∑ P ∈ propositionTwoExceptionalPlaces K L u v, ↑(finiteExtensionPlaceDegree K L P) ≤ ↑chi) (hInfinityCaseI : ∀ (P : ↑(FiniteExtensionInfinityPlace K L)), Sum.inr P ∉ propositionTwoExceptionalPlaces K L u v → (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inr P) < 0 → ↑(h * k + h + k) * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inr P) ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inr P)) (hInfinityCaseII : ∀ (P : ↑(FiniteExtensionInfinityPlace K L)), Sum.inr P ∉ propositionTwoExceptionalPlaces K L u v → 0 ≤ (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inr P) → 0 ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inr P)) (hInfinityCaseIII : ∀ (P : ↑(FiniteExtensionInfinityPlace K L)), Sum.inr P ∈ propositionTwoExceptionalPlaces K L u v → 0 < (finiteExtensionPrincipalDivisor K L v) (Sum.inr P) → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) (Sum.inr P) + ↑(h * k) * (finiteExtensionPrincipalDivisor K L v) (Sum.inr P) + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) (Sum.inr P) - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inr P)) (hInfinityCaseIV : ∀ (P : ↑(FiniteExtensionInfinityPlace K L)), Sum.inr P ∈ propositionTwoExceptionalPlaces K L u v → (finiteExtensionPrincipalDivisor K L v) (Sum.inr P) ≤ 0 → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) (Sum.inr P) + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) (Sum.inr P) - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inr P)) : ↑(finiteExtensionGcdWeightedDegree K L (1 - u) (1 - v)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L v) + ↑k / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L u) + (↑(h * k + h + k) - 1) / 2 * ↑chi

A normalized Frobenius-constant derivation and the four infinity cases imply the exact exhaustive Proposition 2 gcd estimate.