Cases I and II at actual finite extension places

This file supplies the regular-element lifting, finite/perfect residue-field bridge, and scaled-derivation forms of the first two local Corvaja--Zannier Wronskian estimates.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.tempPolynomialAlgebra (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 plane curve auxiliary finite place cases construction.

Equations

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

theorem BGS.CorvajaZannier.tempPolynomialScalarTower (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.tempFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(FunctionField.ringOfIntegers K L)

theorem BGS.CorvajaZannier.tempFiniteIntegralClosureModuleFinite (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) ↥(FunctionField.ringOfIntegers K L)

theorem BGS.CorvajaZannier.tempPolynomialTorsionFreeTop (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.tempFiniteIntegralClosureIsTorsionFree (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) ↥(FunctionField.ringOfIntegers K L)

theorem BGS.CorvajaZannier.tempFiniteIntegralClosureIsDedekindDomain (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] : IsDedekindDomain ↥(FunctionField.ringOfIntegers K L)

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_exists_local_lift_of_orderTop_nonnegative {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] (q : PlaneCurveExtensionFinitePlace K L) (x : L) (hx : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q x) : ∃ (x₀ : FiniteExtensionFinitePlaceLocalRing K L q), x = (finiteExtensionFinitePlaceLocalizationToField q) x₀

theorem BGS.CorvajaZannier.ratFuncFinitePlace_residueField_finite {K : Type u_1} [Field K] [Finite K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : Finite p.asIdeal.ResidueField

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_residueField_finite {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] [Finite K] (q : PlaneCurveExtensionFinitePlace K L) : Finite q.asIdeal.ResidueField

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocal_residueField_perfect {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] [Finite K] (q : PlaneCurveExtensionFinitePlace K L) : PerfectField (IsDiscreteValuationRing.maximalIdeal (FiniteExtensionFinitePlaceLocalRing K L q)).asIdeal.ResidueField

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseII_nonnegative_of_preserves {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] {C : Type u_3} [Field C] [Algebra C L] (q : PlaneCurveExtensionFinitePlace K L) (D : Derivation C L L) (hDIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), D ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (h k : ℕ) (epsilon : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (u v : L) (hu : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q u) (hv : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q v) (hrho : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q ((1 - u) / (1 - v))) : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseII_nonnegative_of_scaled_preserves {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] {C : Type u_3} [Field C] [Algebra C L] (q : PlaneCurveExtensionFinitePlace K L) (h k : ℕ) {n : ℕ} (e : Fin k ⊕ Fin (k + 1) × Fin h ≃ Fin n) (epsilon : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (hepsilon : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilon i = ↑(e i)) (D : Derivation C L L) (c : L) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (u v : L) (hu : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q u) (hv : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q v) (hrho : 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q ((1 - u) / (1 - v))) : 0 ≤ n.choose 2 • finiteExtensionFinitePlaceLocalOrderTop q c + finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseI_q_wronskian_bound_of_scaled_preserves {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 : ℕ} [Fact (Nat.Prime p)] [CharP L p] [Finite K] (q : PlaneCurveExtensionFinitePlace K L) (h k : ℕ) {n : ℕ} (e : Fin k ⊕ Fin (k + 1) × Fin h ≃ Fin n) (epsilonOrder : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (hepsilon : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i = ↑(e i)) (epsilon qBound : ℕ) (D : Derivation (↥(frobeniusSubfield L p)) L L) (c : L) (hScaledIntegral : ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s) (u v : L) (hrhoNe : (1 - u) / (1 - v) ≠ 0) (huOrder : finiteExtensionFinitePlaceLocalOrderTop q u = 0) (hrhoOrder : finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) < 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ finiteExtensionFinitePlaceLocalOrderTop q (u ^ ↑rs.1 * v ^ ↑rs.2)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ qBound) : ↑(↑qBound * finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v))) ≤ n.choose 2 • finiteExtensionFinitePlaceLocalOrderTop q c + finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilonOrder (auxiliaryFamily u v h k)).det