Canonical auxiliary bounds at infinity places

This module transports the four local Corvaja--Zannier auxiliary-family cases to branches above the infinity place of a finite separable extension of RatFunc K. The scaling supplied by the canonical different identifies its local order with the coefficient of finiteExtensionCanonicalDifferentDivisor at .inr P.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityAuxiliaryBaseConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the finite extension canonical auxiliary infinity place construction.

Equations

• BGS.CorvajaZannier.infinityAuxiliaryBaseConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.CorvajaZannier.infinityAuxiliaryBaseConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsScalarTower K (↥(RatFuncInfinityIntegers K)) (RatFunc K)

theorem BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureModuleFinite (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] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityAuxiliaryBaseTorsionFreeTop (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] : Module.IsTorsionFree (↥(RatFuncInfinityIntegers K)) L

theorem BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureIsTorsionFree (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] : Module.IsTorsionFree ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

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

theorem BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncInfinityIntegralClosure K L)) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the finite extension canonical auxiliary infinity place construction.

Equations

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

theorem BGS.CorvajaZannier.infinityAuxiliaryIntegralClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityAuxiliaryBaseFaithfulSmulFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FaithfulSMul (↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityAuxiliaryFractionRingAlgebra (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

The algebra structure from (FractionRing (RatFuncInfinityIntegers K)) to (FractionRing (RatFuncInfinityIntegralClosure K L)) used in the finite extension canonical auxiliary infinity place construction.

Equations

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

theorem BGS.CorvajaZannier.infinityAuxiliaryFractionRingSeparable (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] : Algebra.IsSeparable (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

theorem BGS.CorvajaZannier.infinityAuxiliaryPlaceIsPrime (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (P : ↑(FiniteExtensionInfinityPlace K L)) : (↑P).IsPrime

theorem BGS.CorvajaZannier.infinityAuxiliaryPlaceLiesOver (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (P : ↑(FiniteExtensionInfinityPlace K L)) : (↑P).LiesOver (ratFuncInfinityPlace K).asIdeal

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionInfinityPlaceLocalRing (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 : ↑(FiniteExtensionInfinityPlace K L)) : Type u_2

The localization of the infinity integral closure at one branch.

Equations

• BGS.CorvajaZannier.FiniteExtensionInfinityPlaceLocalRing K L P = Localization.AtPrime (BGS.CorvajaZannier.primeOverHeightOne (BGS.CorvajaZannier.ratFuncInfinityPlace K) P).asIdeal

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalizationToField {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 : ↑(FiniteExtensionInfinityPlace K L)) : FiniteExtensionInfinityPlaceLocalRing K L P →+* L

The map from the localization at an infinity place into the extension field.

Equations

• BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalizationToField P = IsLocalization.lift ⋯

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalizationToField_comp_algebraMap {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 : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionInfinityPlaceLocalizationToField P).comp (algebraMap (↥(RatFuncInfinityIntegralClosure K L)) (FiniteExtensionInfinityPlaceLocalRing K L P)) = algebraMap (↥(RatFuncInfinityIntegralClosure K L)) L

@[reducible]

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalAlgebra {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 : ↑(FiniteExtensionInfinityPlace K L)) : Algebra (FiniteExtensionInfinityPlaceLocalRing K L P) L

The algebra structure on the localized infinity-place ring induced by its map to the field.

Equations

• BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalAlgebra P = (BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalizationToField P).toAlgebra

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalIsFractionRing {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 : ↑(FiniteExtensionInfinityPlace K L)) : have x := finiteExtensionInfinityPlaceLocalAlgebra P; IsFractionRing (FiniteExtensionInfinityPlaceLocalRing K L P) L

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrderTop {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) : WithTop ℤ

The extended local order at an infinity place of the finite extension.

Equations

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

noncomputable def BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrder {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) : ℤ

The integer-valued local order at an infinity place of the finite extension.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrder_eq_globalOrder {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) : finiteExtensionInfinityPlaceLocalOrder P x = finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) x

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrderTop_eq_globalOrder {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) (hx : x ≠ 0) : finiteExtensionInfinityPlaceLocalOrderTop P x = ↑(finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) x)

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrderTop_mul {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 : ↑(FiniteExtensionInfinityPlace K L)) (x y : L) : finiteExtensionInfinityPlaceLocalOrderTop P (x * y) = finiteExtensionInfinityPlaceLocalOrderTop P x + finiteExtensionInfinityPlaceLocalOrderTop P y

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocalOrderTop_pow {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) (n : ℕ) : finiteExtensionInfinityPlaceLocalOrderTop P (x ^ n) = n • finiteExtensionInfinityPlaceLocalOrderTop P x

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_local_preserves_of_global_preserves {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] (P : ↑(FiniteExtensionInfinityPlace K L)) (E : Derivation C L L) (hE : ∀ (t : ↥(RatFuncInfinityIntegralClosure K L)), ∃ (t' : ↥(RatFuncInfinityIntegralClosure K L)), E ((algebraMap (↥(RatFuncInfinityIntegralClosure K L)) L) t) = (algebraMap (↥(RatFuncInfinityIntegralClosure K L)) L) t') (r : FiniteExtensionInfinityPlaceLocalRing K L P) : ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), E ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s

Preservation of the infinity integral closure propagates to the selected localized branch.

theorem BGS.CorvajaZannier.exists_finiteExtensionInfinityPlace_canonicalDifferent_scaling_certificate {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] [Algebra K L] [IsScalarTower K (↥(RatFuncInfinityIntegers K)) L] [IsScalarTower K (↥(RatFuncInfinityIntegralClosure K L)) L] [IsScalarTower (↥(RatFuncInfinityIntegers K)) (↥(RatFuncInfinityIntegralClosure K L)) L] [Algebra K C] [IsScalarTower K C L] (D : Derivation C L L) (Ds : Derivation K ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegers K)) (Es : Derivation K L L) (hEs : ∀ (r : ↥(RatFuncInfinityIntegers K)), Es ((algebraMap (↥(RatFuncInfinityIntegers K)) L) r) = (algebraMap (↥(RatFuncInfinityIntegers K)) L) (Ds r)) (hDX : Derivation.restrictScalars K D = -(algebraMap (↥(RatFuncInfinityIntegers K)) L) (ratFuncInfinityUniformizer K) ^ 2 • Es) (P : ↑(FiniteExtensionInfinityPlace K L)) : ∃ (c : L), c ≠ 0 ∧ finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P) ∧ ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s

The infinity different supplies the exact canonical scaling coefficient. The reciprocal-parameter derivations are explicit inputs: Es preserves the infinity valuation ring and D = -s² Es after restricting constants.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_auxiliaryFamily_caseIII_of_scaled_preserves {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] (P : ↑(FiniteExtensionInfinityPlace 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) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑(↑(k * (k - 1) / 2) * finiteExtensionInfinityPlaceLocalOrder P u + ↑h * ↑k * finiteExtensionInfinityPlaceLocalOrder P v + ↑k * finiteExtensionInfinityPlaceLocalOrder P ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionInfinityPlaceLocalOrder P (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ n.choose 2 • finiteExtensionInfinityPlaceLocalOrderTop P c + finiteExtensionInfinityPlaceLocalOrderTop P (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Infinity-place source case (iii), after scaling a global derivation by a factor preserving the infinity integral closure.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_auxiliaryFamily_caseIV_of_scaled_preserves {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] (P : ↑(FiniteExtensionInfinityPlace 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) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑(↑(k * (k - 1) / 2) * finiteExtensionInfinityPlaceLocalOrder P u + ↑k * finiteExtensionInfinityPlaceLocalOrder P ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionInfinityPlaceLocalOrder P (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ n.choose 2 • finiteExtensionInfinityPlaceLocalOrderTop P c + finiteExtensionInfinityPlaceLocalOrderTop P (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Infinity-place source case (iv), with the same exact scaling correction.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_inr_eq_infinityPlaceOrder {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] (x : L) (P : ↑(FiniteExtensionInfinityPlace K L)) : (finiteExtensionPrincipalDivisor K L x) (Sum.inr P) = finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) x

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_canonicalAuxiliary_caseIII_of_scaling {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] (P : ↑(FiniteExtensionInfinityPlace K L)) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hcOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P)) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) 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.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)

Infinity source case (iii), expressed with the actual canonical different coefficient and exhaustive principal divisors.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_canonicalAuxiliary_caseIV_of_scaling {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] (P : ↑(FiniteExtensionInfinityPlace K L)) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hcOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P)) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) 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.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)

Infinity source case (iv), in the same canonical global-divisor form.

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_exists_local_lift_of_orderTop_nonnegative {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 : ↑(FiniteExtensionInfinityPlace K L)) (x : L) (hx : 0 ≤ finiteExtensionInfinityPlaceLocalOrderTop P x) : ∃ (x₀ : FiniteExtensionInfinityPlaceLocalRing K L P), x = (finiteExtensionInfinityPlaceLocalizationToField P) x₀

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_auxiliaryFamily_caseII_of_scaled_preserves {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] (P : ↑(FiniteExtensionInfinityPlace 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) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s) (u v : L) (hu : 0 ≤ finiteExtensionInfinityPlaceLocalOrderTop P u) (hv : 0 ≤ finiteExtensionInfinityPlaceLocalOrderTop P v) (hrho : 0 ≤ finiteExtensionInfinityPlaceLocalOrderTop P ((1 - u) / (1 - v))) : 0 ≤ n.choose 2 • finiteExtensionInfinityPlaceLocalOrderTop P c + finiteExtensionInfinityPlaceLocalOrderTop P (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_canonicalAuxiliary_caseII_of_scaling {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] (P : ↑(FiniteExtensionInfinityPlace K L)) (D : Derivation C L L) (c : L) (hc : c ≠ 0) (hcOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P)) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s) (h k : ℕ) (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (huOrder : 0 ≤ finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) u) (hvOrder : 0 ≤ finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) v) (hrhoOrder : 0 ≤ finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) ((1 - u) / (1 - v))) (hW : (indexedDedekindLocalWronskian D (auxiliaryFamilyDerivativeOrder h k) (auxiliaryFamily u v h k)).det ≠ 0) : 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)

theorem BGS.CorvajaZannier.ratFuncInfinityPlace_residueField_finite {K : Type u_1} [Field K] [DecidableEq (RatFunc K)] [Finite K] : Finite (ratFuncInfinityPlace K).asIdeal.ResidueField

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_residueField_finite {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] [Finite K] (P : ↑(FiniteExtensionInfinityPlace K L)) : Finite (↑P).ResidueField

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlaceLocal_residueField_perfect {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] [Finite K] (P : ↑(FiniteExtensionInfinityPlace K L)) : PerfectField (IsDiscreteValuationRing.maximalIdeal (FiniteExtensionInfinityPlaceLocalRing K L P)).asIdeal.ResidueField

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_auxiliaryFamily_caseI_of_scaled_preserves {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] (P : ↑(FiniteExtensionInfinityPlace 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) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) s) (u v : L) (hrhoNe : (1 - u) / (1 - v) ≠ 0) (huOrder : finiteExtensionInfinityPlaceLocalOrderTop P u = 0) (hrhoOrder : finiteExtensionInfinityPlaceLocalOrder P ((1 - u) / (1 - v)) < 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ finiteExtensionInfinityPlaceLocalOrderTop P (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 * finiteExtensionInfinityPlaceLocalOrder P ((1 - u) / (1 - v))) ≤ n.choose 2 • finiteExtensionInfinityPlaceLocalOrderTop P c + finiteExtensionInfinityPlaceLocalOrderTop P (indexedDedekindLocalWronskian D epsilonOrder (auxiliaryFamily u v h k)).det

theorem BGS.CorvajaZannier.finiteExtensionInfinityPlace_canonicalAuxiliary_caseI_of_scaling {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] (P : ↑(FiniteExtensionInfinityPlace K L)) (D : Derivation (↥(frobeniusSubfield L p)) L L) (c : L) (hc : c ≠ 0) (hcOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inr P)) (hScaledLocal : ∀ (r : FiniteExtensionInfinityPlaceLocalRing K L P), ∃ (s : FiniteExtensionInfinityPlaceLocalRing K L P), (c • D) ((finiteExtensionInfinityPlaceLocalizationToField P) r) = (finiteExtensionInfinityPlaceLocalizationToField P) 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 (primeOverHeightOne (ratFuncInfinityPlace K) P) u = 0) (hvOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) v = 0) (hrhoOrder : finitePlaceOrder (primeOverHeightOne (ratFuncInfinityPlace K) P) ((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.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)