Local reciprocal normalization for an irreducible plane curve

This file specializes LocalReciprocalDiscriminant to the first-coordinate model of an irreducible plane curve. When the second-coordinate degree is smaller than the cardinality of the constant field, at each finite prime of K[X] it selects a local center at which the defining polynomial has unit value. This includes explicit finite-field and infinite-field interfaces. It also proves the defining relation, primitive generation, and the exact extension degree over K(X). The final theorem identifies the minimal polynomial of the reciprocal local parameter with the unit-normalized reciprocal translate of the localized plane equation.

@[simp]

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_X_zero {K : Type u_1} [Field K] : planeCurvePolynomialInSecondCoordinate (MvPolynomial.X 0) = Polynomial.C Polynomial.X

Coordinate 0 becomes the coefficient variable in the iterated plane curve presentation.

@[simp]

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_X_one {K : Type u_1} [Field K] : planeCurvePolynomialInSecondCoordinate (MvPolynomial.X 1) = Polynomial.X

Coordinate 1 becomes the outer polynomial variable.

@[simp]

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_C {K : Type u_1} [Field K] (c : K) : planeCurvePolynomialInSecondCoordinate (MvPolynomial.C c) = Polynomial.C (Polynomial.C c)

Constants remain constants in both polynomial variables.

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_eq_bivariateEquiv {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : planeCurvePolynomialInSecondCoordinate f = (Polynomial.Bivariate.equivMvPolynomial K).symm f

The plane-curve presentation agrees with Mathlib's standard bivariate polynomial equivalence.

theorem BGS.CorvajaZannier.eval₂_planeCurvePolynomialInSecondCoordinate {K : Type u_1} [Field K] {A : Type u_2} [CommSemiring A] [Algebra K A] (f : MvPolynomial (Fin 2) K) (x y : A) : Polynomial.eval₂ (Polynomial.eval₂RingHom (algebraMap K A) x) y (planeCurvePolynomialInSecondCoordinate f) = MvPolynomial.eval₂ (algebraMap K A) ![x, y] f

Evaluation of the iterated polynomial is ordinary two-coordinate evaluation of the original multivariate polynomial.

noncomputable def BGS.CorvajaZannier.localizationAtPrimeToRatFunc {K : Type u_1} [Field K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : Localization.AtPrime p.asIdeal →+* RatFunc K

The canonical inclusion of the local ring of K[X] at a finite prime into its fraction field K(X).

Equations

• BGS.CorvajaZannier.localizationAtPrimeToRatFunc p = IsLocalization.lift ⋯

@[simp]

theorem BGS.CorvajaZannier.localizationAtPrimeToRatFunc_comp_algebraMap {K : Type u_1} [Field K] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : (localizationAtPrimeToRatFunc p).comp (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) = algebraMap (Polynomial K) (RatFunc K)

The local inclusion extends the standard polynomial inclusion in RatFunc K.

theorem BGS.CorvajaZannier.exists_localized_center_eval_isUnit_of_natDegree_lt_card {K : Type u_1} [Field K] (F : Polynomial (Polynomial K)) (hF : F.IsPrimitive) (hcardK : ↑F.natDegree < Cardinal.mk K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) F))

A primitive polynomial over K[X] has a unit value at some center in every finite localization when its degree is smaller than the cardinality of the constant field.

theorem BGS.CorvajaZannier.exists_localized_center_eval_isUnit {K : Type u_1} [Field K] [Infinite K] (F : Polynomial (Polynomial K)) (hF : F.IsPrimitive) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) F))

Infinite constant fields automatically satisfy the cardinality hypothesis for a primitive polynomial of finite degree.

theorem BGS.CorvajaZannier.exists_localized_center_eval_isUnit_of_natDegree_lt_fintypeCard {K : Type u_1} [Field K] [Fintype K] (F : Polynomial (Polynomial K)) (hF : F.IsPrimitive) (hcardK : F.natDegree < Fintype.card K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) F))

Finite constant fields satisfy the local center hypothesis as soon as the polynomial degree is smaller than the field cardinality.

theorem BGS.CorvajaZannier.exists_planeCurve_localized_center_eval_isUnit_of_degreeOf_second_lt_card {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hcardK : ↑(MvPolynomial.degreeOf 1 f) < Cardinal.mk K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) (planeCurvePolynomialInSecondCoordinate f)))

The irreducible plane equation admits a unit-valued center at every finite first-coordinate prime when its second-coordinate degree is smaller than the cardinality of the constant field.

theorem BGS.CorvajaZannier.exists_planeCurve_localized_center_eval_isUnit {K : Type u_1} [Field K] [Infinite K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) (planeCurvePolynomialInSecondCoordinate f)))

Over an infinite constant field, every finite first-coordinate prime has a unit-valued plane-curve center.

theorem BGS.CorvajaZannier.exists_planeCurve_localized_center_eval_isUnit_of_degreeOf_second_lt_fintypeCard {K : Type u_1} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ∃ (a : Polynomial K), IsUnit (Polynomial.eval ((algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) a) (Polynomial.map (algebraMap (Polynomial K) (Localization.AtPrime p.asIdeal)) (planeCurvePolynomialInSecondCoordinate f)))

Over a finite constant field, the plane-curve center exists under the literal degree-versus-cardinality inequality.

theorem BGS.CorvajaZannier.aeval_planeCurvePolynomialInSecondCoordinate_ratFunc_eq_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; (Polynomial.aeval (planeCurveFunction f 1)) (Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (planeCurvePolynomialInSecondCoordinate f)) = 0

The second coordinate is a root of the defining equation after extending the first-coordinate coefficients to K(X).

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_ratFunc_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : Irreducible (Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (planeCurvePolynomialInSecondCoordinate f))

The defining equation remains irreducible over K(X).

theorem BGS.CorvajaZannier.adjoin_secondCoordinate_over_firstRatFunc_eq_top {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; (RatFunc K)[planeCurveFunction f 1] = ⊤

The second coordinate primitively generates the plane function field over the first-coordinate copy of K(X).

theorem BGS.CorvajaZannier.planeCurve_local_reciprocal_certificate_of_degreeOf_second_lt_card {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : ↑(MvPolynomial.degreeOf 1 f) < Cardinal.mk K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : have hx := ⋯; let A := Localization.AtPrime p.asIdeal; have ι := localizationAtPrimeToRatFunc p; have G := Polynomial.map (algebraMap (Polynomial K) A) (planeCurvePolynomialInSecondCoordinate f); ∃ (a : Polynomial K) (u : Aˣ), have c := (algebraMap (Polynomial K) A) a; Polynomial.eval c G = ↑u ∧ Polynomial.eval₂ ((algebraMap (RatFunc K) (PlaneCurveFunctionField f)).comp ι) (planeCurveFunction f 1) G = 0 ∧ planeCurveFunction f 1 ≠ (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) (ι c) ∧ (RatFunc K)[planeCurveFunction f 1] = ⊤ ∧ G.natDegree = Module.finrank (RatFunc K) (PlaneCurveFunctionField f)

All local hypotheses for reciprocal normalization, packaged with an explicit center and unit, under the exact cardinality hypothesis needed for center selection.

theorem BGS.CorvajaZannier.planeCurve_local_reciprocal_certificate_of_degreeOf_second_lt_fintypeCard {K : Type u_1} [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) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : have hx := ⋯; let A := Localization.AtPrime p.asIdeal; have ι := localizationAtPrimeToRatFunc p; have G := Polynomial.map (algebraMap (Polynomial K) A) (planeCurvePolynomialInSecondCoordinate f); ∃ (a : Polynomial K) (u : Aˣ), have c := (algebraMap (Polynomial K) A) a; Polynomial.eval c G = ↑u ∧ Polynomial.eval₂ ((algebraMap (RatFunc K) (PlaneCurveFunctionField f)).comp ι) (planeCurveFunction f 1) G = 0 ∧ planeCurveFunction f 1 ≠ (algebraMap (RatFunc K) (PlaneCurveFunctionField f)) (ι c) ∧ (RatFunc K)[planeCurveFunction f 1] = ⊤ ∧ G.natDegree = Module.finrank (RatFunc K) (PlaneCurveFunctionField f)

Finite-field form of the full reciprocal-normalization certificate.

theorem BGS.CorvajaZannier.planeCurve_minpoly_reciprocal_local_normalization_of_degreeOf_second_lt_card {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : ↑(MvPolynomial.degreeOf 1 f) < Cardinal.mk K) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : have hx := ⋯; 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)

At every finite first-coordinate prime, a reciprocal translate of the localized plane equation is exactly the minimal polynomial of the reciprocal local parameter, under the exact cardinality hypothesis needed to select its center.

theorem BGS.CorvajaZannier.planeCurve_minpoly_reciprocal_local_normalization_of_degreeOf_second_lt_fintypeCard {K : Type u_1} [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) (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : have hx := ⋯; 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)

Finite-field form of the reciprocal minimal-polynomial normalization.