Canonical finite-place bounds for a normalized derivation

The raw local Wronskian estimates accept an arbitrary clearing scalar. This file chooses that scalar from the different at each finite place, so its order is definitionally replaced by the coefficient of the canonical different divisor. These are the four finite-place inputs used by the exhaustive global summation.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.normalizedCasesPolynomialAlgebra (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 auxiliary finite place normalized construction.

Equations

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

theorem BGS.CorvajaZannier.normalizedCasesPolynomialScalarTower (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.normalizedCasesFiniteIntegralClosureModuleFinite (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.normalizedCasesFiniteIntegralClosureIsIntegral (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.normalizedCasesPolynomialTorsionFreeTop (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.normalizedCasesFiniteIntegralClosureIsTorsionFree (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)

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.normalizedFinitePlaceCanonicalDifferent (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] : FiniteExtensionPlace K L →₀ ℤ

The canonical different divisor used by the normalized finite-place estimates.

Equations

• BGS.CorvajaZannier.normalizedFinitePlaceCanonicalDifferent K L = BGS.CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseI_of_normalized (K : Type u_1) [Field K] [Finite 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] (q : FiniteExtensionFinitePlace K L) (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (h k : ℕ) (hn : 0 < h * k + h + k) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (huOrder : finitePlaceOrder q u = 0) (hvOrder : finitePlaceOrder q v = 0) (hrhoOrder : finitePlaceOrder q ((1 - u) / (1 - v)) < 0) (hW : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) : ↑(h * k + h + k) * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inl q) ≤ ↑((h * k + h + k).choose 2) * (normalizedFinitePlaceCanonicalDifferent K L) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Canonical finite-place case (i), outside the exceptional set with a pole of (1-u)/(1-v).

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseII_of_normalized (K : Type u_1) [Field K] [Finite 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] (q : FiniteExtensionFinitePlace K L) (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (h k : ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (huOrder : 0 ≤ finitePlaceOrder q u) (hvOrder : 0 ≤ finitePlaceOrder q v) (hrhoOrder : 0 ≤ finitePlaceOrder q ((1 - u) / (1 - v))) (hW : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) : 0 ≤ ↑((h * k + h + k).choose 2) * (normalizedFinitePlaceCanonicalDifferent K L) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Canonical finite-place case (ii), outside the exceptional set without a pole of (1-u)/(1-v).

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseIII_of_normalized (K : Type u_1) [Field K] [Finite 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] (q : FiniteExtensionFinitePlace K L) (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (h k : ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (hW : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) : ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) (Sum.inl q) + ↑(h * k) * (finiteExtensionPrincipalDivisor K L v) (Sum.inl q) + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) (Sum.inl q) - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (normalizedFinitePlaceCanonicalDifferent K L) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Canonical finite-place case (iii), at a positive-order place of v.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseIV_of_normalized (K : Type u_1) [Field K] [Finite 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] (q : FiniteExtensionFinitePlace K L) (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (h k : ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (hW : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) : ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) (Sum.inl q) + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) (Sum.inl q) - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (normalizedFinitePlaceCanonicalDifferent K L) (Sum.inl q) + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Canonical finite-place case (iv), at a nonpositive-order place of v.