Finite-place cases for the canonical auxiliary family

Prove the local auxiliary-family inequalities at finite places, including the grid-order and derivative-order sums.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.finiteCanonicalCasesPolynomialAlgebra (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 construction.

Equations

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

theorem BGS.CorvajaZannier.finiteCanonicalCasesPolynomialScalarTower (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.finiteCanonicalCasesFiniteIntegralClosureModuleFinite (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.finiteCanonicalCasesFiniteIntegralClosureIsIntegral (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.finiteCanonicalCasesPolynomialTorsionFreeTop (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.finiteCanonicalCasesFiniteIntegralClosureIsTorsionFree (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.finiteExtensionFinitePlace_canonicalAuxiliary_caseI (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] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] [Finite K] (q : FiniteExtensionFinitePlace K L) (D : Derivation (↥(frobeniusSubfield L p)) L L) (c : L) (hc : c ≠ 0) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (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) * finitePlaceOrder q c + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Finite-place source case (i), specialized to the consecutive derivative orders on the source auxiliary family.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseII (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] (q : FiniteExtensionFinitePlace K L) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (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) * finitePlaceOrder q c + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Finite-place source case (ii), with every local order converted to the coefficient used by the exhaustive principal divisor.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseIII (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] (q : FiniteExtensionFinitePlace K L) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (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) * finitePlaceOrder q c + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Finite-place source case (iii), expressed directly with the global principal divisor and the consecutive-order Wronskian.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_canonicalAuxiliary_caseIV (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] (q : FiniteExtensionFinitePlace K L) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (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) * finitePlaceOrder q c + (finiteExtensionPrincipalDivisor K L (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det) (Sum.inl q)

Finite-place source case (iv), in the same global-divisor form.