Auxiliary Wronskian bounds at finite plane-curve places

This file connects the uniformizer-free local Corvaja--Zannier estimates to the actual finite primes of the integral closure in a finite extension of K(X). The constants used for the local derivation-extension step are the ground field K; the Wronskian derivation may subsequently be obtained by restricting scalars from the Frobenius constant field. Thus no algebra map from the Frobenius constant field to a nontrivial DVR is required.

The unramified local-preservation bridge

theorem BGS.CorvajaZannier.dedekindLocal_ambientDerivation_preserves_of_not_dvd_different {A : Type u_1} {B : Type u_2} {C : Type u_3} {U : Type u_4} [CommRing A] [CommRing B] [CommRing C] [CommRing U] [IsDedekindDomain A] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (p : Ideal A) (Q : Ideal B) [p.IsPrime] [Q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime Q)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime Q)] [Algebra C (Localization.AtPrime p)] [Algebra C (Localization.AtPrime Q)] [Algebra C U] [Algebra (Localization.AtPrime p) U] [Algebra (Localization.AtPrime Q) U] [IsScalarTower C (Localization.AtPrime p) (Localization.AtPrime Q)] [IsScalarTower C (Localization.AtPrime Q) U] [IsScalarTower (Localization.AtPrime p) (Localization.AtPrime Q) U] (hQ : ¬Q ∣ differentIdeal A B) (D : Derivation C (Localization.AtPrime p) (Localization.AtPrime p)) (E : Derivation C U U) (hE : ∀ (s : Localization.AtPrime p), E ((algebraMap (Localization.AtPrime p) U) s) = (algebraMap (Localization.AtPrime p) U) (D s)) (t : Localization.AtPrime Q) : ∃ (t' : Localization.AtPrime Q), E ((algebraMap (Localization.AtPrime Q) U) t) = (algebraMap (Localization.AtPrime Q) U) t'

Outside the different, the ambient derivation preserves the selected extension DVR. This is the existential-preservation form consumed by the uniformizer-free Wronskian estimates. In the plane-curve application C is the ground field K (after restricting scalars from L^p), so all local algebra structures here are genuine; no map L^p → B_Q is requested.

@[instance_reducible]

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

Equations

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

theorem BGS.CorvajaZannier.auxiliaryFinitePlacePolynomialScalarTower (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.auxiliaryFinitePlaceFiniteIntegralClosureIsIntegral (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.auxiliaryFinitePlaceFiniteIntegralClosureModuleFinite (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.auxiliaryFinitePlacePolynomialTorsionFreeTop (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.auxiliaryFinitePlaceFiniteIntegralClosureIsTorsionFree (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.auxiliaryFinitePlaceFiniteIntegralClosureIsDedekindDomain (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)

@[reducible, inline]

abbrev BGS.CorvajaZannier.PlaneCurveExtensionFinitePlace (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Type u_2

The actual finite places of L / K(X), before adjoining the places over infinity. This is definitionally the finite summand used by the exhaustive place infrastructure.

Equations

• BGS.CorvajaZannier.PlaneCurveExtensionFinitePlace K L = IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers K L)

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionFinitePlaceBaseLocalRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : Type u_1

The base local ring at a finite place of the extension.

Equations

• BGS.CorvajaZannier.FiniteExtensionFinitePlaceBaseLocalRing K L q = Localization.AtPrime (IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q).asIdeal

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionFinitePlaceLocalRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : Type u_2

The corresponding local ring of the extension at that finite place.

Equations

• BGS.CorvajaZannier.FiniteExtensionFinitePlaceLocalRing K L q = Localization.AtPrime q.asIdeal

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalizationToField {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : FiniteExtensionFinitePlaceLocalRing K L q →+* L

Canonical inclusion of the localization at an actual finite extension place into the ambient function field.

Equations

• BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalizationToField q = IsLocalization.lift ⋯

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalizationToField_comp_algebraMap {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : (finiteExtensionFinitePlaceLocalizationToField q).comp (algebraMap (↥(FunctionField.ringOfIntegers K L)) (FiniteExtensionFinitePlaceLocalRing K L q)) = algebraMap (↥(FunctionField.ringOfIntegers K L)) L

@[reducible]

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalAlgebra {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : Algebra (FiniteExtensionFinitePlaceLocalRing K L q) L

The canonical algebra structure on the ambient function field from the localized finite-place DVR.

Equations

• BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalAlgebra q = (BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalizationToField q).toAlgebra

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalIsFractionRing {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] (q : PlaneCurveExtensionFinitePlace K L) : IsFractionRing (FiniteExtensionFinitePlaceLocalRing K L q) L

The ambient function field is the fraction field of every finite-place localization.

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrderTop {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) : WithTop ℤ

The normalized order on the localization at an actual finite place of L / K(X). Keeping this definition attached to q avoids introducing a spurious algebra structure from the Frobenius constant field to the DVR.

Equations

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

noncomputable def BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrder {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) : ℤ

Integer-valued form of the localized order.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrder_eq_globalOrder {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) : finiteExtensionFinitePlaceLocalOrder q x = finitePlaceOrder q x

The order used by the actual localized DVR bound is exactly the global height-one order of the same finite place.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrderTop_eq_globalOrder {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 : x ≠ 0) : finiteExtensionFinitePlaceLocalOrderTop q x = ↑(finitePlaceOrder q x)

Nonzero localized WithTop orders are the corresponding global height-one orders.

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrderTop_mul {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 y : L) : finiteExtensionFinitePlaceLocalOrderTop q (x * y) = finiteExtensionFinitePlaceLocalOrderTop q x + finiteExtensionFinitePlaceLocalOrderTop q y

@[simp]

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrderTop_pow {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) (n : ℕ) : finiteExtensionFinitePlaceLocalOrderTop q (x ^ n) = n • finiteExtensionFinitePlaceLocalOrderTop q x

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIII_source_lower_bound_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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + (h * k) • finiteExtensionFinitePlaceLocalOrder q v + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Source case (iii), now indexed by an actual finite place of the integral closure. The sole local hypothesis says that the derivation preserves the localized DVR; it does not ask for an algebra map C → R_q.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIV_source_lower_bound_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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Source case (iv), indexed by an actual finite place of the integral closure and requiring only preservation of its localized DVR.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIII_source_lower_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] {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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + (h * k) • finiteExtensionFinitePlaceLocalOrder q v + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ n.choose 2 • finiteExtensionFinitePlaceLocalOrderTop q c + finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Source case (iii) for a global derivation after multiplying it by the local correction factor c. The displayed right side has been transported back to the original global Wronskian and records the exact triangular correction choose(n,2) * ord_q(c).

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIV_source_lower_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] {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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ n.choose 2 • finiteExtensionFinitePlaceLocalOrderTop q c + finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Source case (iv) with the same exact local correction term.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIII_source_lower_bound_of_restrictScalars_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] [Algebra K C] [Algebra K L] [IsScalarTower K 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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + (h * k) • finiteExtensionFinitePlaceLocalOrder q v + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Case (iii) for a derivation over a larger constant field (in the application, C = L^p). The proof restricts scalars to K before invoking the local DVR theorem, while the displayed Wronskian is still the original C-derivation Wronskian because restriction does not change its function.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlace_auxiliaryFamily_caseIV_source_lower_bound_of_restrictScalars_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] [Algebra K C] [Algebra K L] [IsScalarTower K 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 : u ≠ 0) (hv : v ≠ 0) (hu1 : u ≠ 1) (hv1 : v ≠ 1) : ↑((k * (k - 1) / 2) • finiteExtensionFinitePlaceLocalOrder q u + k • finiteExtensionFinitePlaceLocalOrder q ((1 - u) / (1 - v)) + ∑ rs : Fin (k + 1) × Fin h, finiteExtensionFinitePlaceLocalOrder q (u ^ ↑rs.1 * v ^ ↑rs.2) - ∑ i : Fin k ⊕ Fin (k + 1) × Fin h, ↑(epsilon i)) ≤ finiteExtensionFinitePlaceLocalOrderTop q (indexedDedekindLocalWronskian D epsilon (auxiliaryFamily u v h k)).det

Case (iv) after the same honest restriction of constants from C to the ground field K.

Plane-curve reciprocal normalization at a selected extension place

theorem BGS.CorvajaZannier.planeCurve_minpoly_reciprocal_local_normalization_at_finiteExtensionPlace {K : Type u_3} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) : have hx := ⋯; ∀ (q : PlaneCurveExtensionFinitePlace K (PlaneCurveFunctionField f)), have p := IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) q; let A := Localization.AtPrime p.asIdeal; have ι := localizationAtPrimeToRatFunc p; ∃ (a : Polynomial K) (u : Aˣ), have c := (algebraMap (Polynomial K) A) a; have G := Polynomial.map (algebraMap (Polynomial K) A) (planeCurvePolynomialInSecondCoordinate f); minpoly (RatFunc K) (planeCurveFunction f 1 - (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) (ι c))⁻¹ = Polynomial.map ι (unitNormalizedReciprocalTranslate G c u)

The reciprocal minimal-polynomial normalization, with the base prime selected as the prime lying below an actual finite place of the plane-curve function field. This is the local primitive-element/different certificate paired with the Wronskian estimates above.