Normalized global derivations for the canonical argument

Construct the rational-function derivations and reciprocal-chart estimates used to normalize the global canonical Wronskian argument.

@[instance_reducible]

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

Equations

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

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

noncomputable def BGS.CorvajaZannier.probeRatFuncDerivation (K : Type u_1) [Field K] : Derivation K (RatFunc K) (RatFunc K)

The derivation on rational functions used to normalize the auxiliary construction.

Equations

• BGS.CorvajaZannier.probeRatFuncDerivation K = BGS.CorvajaZannier.formallyEtaleDerivationExtension ((Polynomial.mkDerivation K) 1)

@[simp]

theorem BGS.CorvajaZannier.probeRatFuncDerivation_algebraMap (K : Type u_1) [Field K] (f : Polynomial K) : (probeRatFuncDerivation K) ((algebraMap (Polynomial K) (RatFunc K)) f) = (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.derivative f)

theorem BGS.CorvajaZannier.probeRatFuncDerivation_eq (K : Type u_1) [Field K] (x : RatFunc K) : (probeRatFuncDerivation K) x = ((algebraMap (Polynomial K) (RatFunc K)) x.denom)⁻¹ ^ 2 * (algebraMap (Polynomial K) (RatFunc K)) (x.denom * Polynomial.derivative x.num - x.num * Polynomial.derivative x.denom)

theorem BGS.CorvajaZannier.probeRatFuncDerivation_intDegree_le_sub_one (K : Type u_1) [Field K] (x : RatFunc K) (hx : x ≠ 0) (hDx : (probeRatFuncDerivation K) x ≠ 0) : ((probeRatFuncDerivation K) x).intDegree ≤ x.intDegree - 1

noncomputable def BGS.CorvajaZannier.probeRatFuncReciprocalDerivation (K : Type u_1) [Field K] : Derivation K (RatFunc K) (RatFunc K)

The derivation of reciprocal rational functions used at infinity.

Equations

• BGS.CorvajaZannier.probeRatFuncReciprocalDerivation K = -RatFunc.X ^ 2 • BGS.CorvajaZannier.probeRatFuncDerivation K

@[simp]

theorem BGS.CorvajaZannier.probeRatFuncReciprocalDerivation_apply (K : Type u_1) [Field K] (x : RatFunc K) : (probeRatFuncReciprocalDerivation K) x = -RatFunc.X ^ 2 * (probeRatFuncDerivation K) x

theorem BGS.CorvajaZannier.probeRatFuncReciprocalDerivation_intDegree_nonpositive_of_negative (K : Type u_1) [Field K] (x : RatFunc K) (hxDegree : x.intDegree < 0) : ((probeRatFuncReciprocalDerivation K) x).intDegree ≤ 0

theorem BGS.CorvajaZannier.probeRatFuncReciprocalDerivation_mem_infinityIntegers (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (r : ↥(RatFuncInfinityIntegers K)) : (probeRatFuncReciprocalDerivation K) ↑r ∈ RatFuncInfinityIntegers K

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

The derivation induced on the infinity-place integer ring.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.probeInfinityRingDerivation_coe (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (r : ↥(RatFuncInfinityIntegers K)) : ↑((probeInfinityRingDerivation K) r) = (probeRatFuncReciprocalDerivation K) ↑r

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probeConstantAlgebraL (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the finite extension canonical global normalized automatic construction.

Equations

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

theorem BGS.CorvajaZannier.probeConstantRatFuncTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.CorvajaZannier.probeInfinityConstantLTower (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)) L

@[instance_reducible]

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

Equations

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

theorem BGS.CorvajaZannier.probeInfinityClosureConstantBaseTower (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.probeInfinityClosureToFieldTower (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (↥(RatFuncInfinityIntegers K)) (↥(RatFuncInfinityIntegralClosure K L)) L

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

theorem BGS.CorvajaZannier.probeInfinityClosureModuleFinite (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.probeInfinityClosureIsIntegral (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.probeInfinityBaseTorsionFreeTop (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.probeInfinityClosureIsTorsionFree (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.probeInfinityClosureIsDedekindDomain (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.probeInfinityClosureIsFractionRing (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.probePolynomialLAlgebra (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 automatic construction.

Equations

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

theorem BGS.CorvajaZannier.probePolynomialRatFuncLTower (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.probePolynomialConstantLTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) L

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.probeFrobeniusConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] : Algebra K ↥(frobeniusSubfield L p)

The algebra structure from K to (frobeniusSubfield L p) used in the finite extension canonical global normalized automatic construction.

Equations

• BGS.CorvajaZannier.probeFrobeniusConstantAlgebra K L = BGS.CorvajaZannier.perfectConstantsToFrobeniusSubfield.toAlgebra

theorem BGS.CorvajaZannier.probeFrobeniusConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] : IsScalarTower K (↥(frobeniusSubfield L p)) L

theorem BGS.CorvajaZannier.probe_normalizedDerivation_comp_ratFunc (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) : Derivation.compAlgebraMap (RatFunc K) (Derivation.restrictScalars K D) = (Algebra.linearMap (RatFunc K) L).compDer (probeRatFuncDerivation K)

noncomputable def BGS.CorvajaZannier.probeAmbientReciprocalDerivation (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] (D : Derivation (↥(frobeniusSubfield L p)) L L) : Derivation K L L

The reciprocal derivation transported to the ambient extension field.

Equations

• BGS.CorvajaZannier.probeAmbientReciprocalDerivation K L D = -(algebraMap (RatFunc K) L) RatFunc.X ^ 2 • Derivation.restrictScalars K D

theorem BGS.CorvajaZannier.probeAmbientReciprocalDerivation_extends (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (r : ↥(RatFuncInfinityIntegers K)) : (probeAmbientReciprocalDerivation K L D) ((algebraMap (↥(RatFuncInfinityIntegers K)) L) r) = (algebraMap (↥(RatFuncInfinityIntegers K)) L) ((probeInfinityRingDerivation K) r)

theorem BGS.CorvajaZannier.probeAmbientReciprocalDerivation_changeParameter (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] (D : Derivation (↥(frobeniusSubfield L p)) L L) : Derivation.restrictScalars K D = -(algebraMap (↥(RatFuncInfinityIntegers K)) L) (ratFuncInfinityUniformizer K) ^ 2 • probeAmbientReciprocalDerivation K L D

theorem BGS.CorvajaZannier.probe_exists_normalizedInfinityScaling (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 K p] [CharP L p] [PerfectField K] (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (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

theorem BGS.CorvajaZannier.globalInfinityClosureModuleFinite (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.globalInfinityClosureIsIntegral (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.globalInfinityBaseTorsionFreeTop (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.globalInfinityClosureIsTorsionFree (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.globalInfinityClosureIsDedekindDomain (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.globalInfinityClosureIsFractionRing (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

theorem BGS.CorvajaZannier.finiteExtensionGcdBound_of_normalizedCanonicalPlacewiseBounds (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] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [Finite K] (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) : ↑(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

The exact exhaustive Proposition 2 gcd estimate from a normalized Frobenius-constant derivation. The infinity-place hypotheses of finiteExtensionGcdBound_of_normalizedCanonicalInfinityPlacewiseBounds are automatic: the reciprocal derivation at infinity gives the change of parameter, and the different supplies the canonical clearing scalar.