The actual powered-coordinate image curve

For a plane curve with function-field coordinates x,y, this file defines the intermediate field K(x^m,y^n) and controls its two projection degrees. It then transports the minimal polynomial of y^n over K(x^m) to the standard rational-function field, clears denominators, takes the primitive part, and applies Gauss' lemma. The resulting polynomial in K[U,V] is irreducible, vanishes at (x^m,y^n), and has coordinate degrees exactly the two projection degrees of the powered image.

Consequently its degree in y^n is at most m * degreeOf 1 f, while its degree in x^m is at most n * degreeOf 0 f. This is the source-sensitive elimination input needed for the Corvaja--Zannier middle game.

theorem BGS.CorvajaZannier.adjoin_pow_le_adjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (m : ℕ) : K⟮z ^ m⟯ ≤ K⟮z⟯

theorem BGS.CorvajaZannier.restrictScalars_adjoin_over_adjoin_pow_eq_adjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (m : ℕ) : IntermediateField.restrictScalars K (↥K⟮z ^ m⟯)⟮z⟯ = K⟮z⟯

theorem BGS.CorvajaZannier.finrank_adjoin_over_adjoin_pow_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (m : ℕ) (hm : 0 < m) : Module.finrank ↥K⟮z ^ m⟯ ↥(↥K⟮z ^ m⟯)⟮z⟯ ≤ m

theorem BGS.CorvajaZannier.finiteDimensional_over_adjoin_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (m : ℕ) (hm : 0 < m) [FiniteDimensional (↥K⟮z⟯) L] : FiniteDimensional (↥K⟮z ^ m⟯) L

theorem BGS.CorvajaZannier.finrank_over_adjoin_pow_le_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (z : L) (m d : ℕ) (hm : 0 < m) [FiniteDimensional (↥K⟮z⟯) L] (hdegree : Module.finrank (↥K⟮z⟯) L ≤ d) : Module.finrank (↥K⟮z ^ m⟯) L ≤ m * d

Clearing the minimal polynomial over a rational coordinate field

noncomputable def BGS.CorvajaZannier.ratFuncMinpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) : Polynomial (RatFunc K)

Transport the minimal polynomial of v over K(u) to the standard rational-function field K(X).

Equations

• BGS.CorvajaZannier.ratFuncMinpoly u hu v = Polynomial.map (↑(RatFunc.algEquivOfTranscendental u hu).symm.toRingEquiv) (minpoly (↥K⟮u⟯) v)

noncomputable def BGS.CorvajaZannier.integerClearedMinpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) : Polynomial (Polynomial K)

Clear the coefficient denominators in the transported minimal polynomial. This is an iterated polynomial over K.

Equations

• BGS.CorvajaZannier.integerClearedMinpoly u hu v = IsLocalization.integerNormalization (nonZeroDivisors (Polynomial K)) (BGS.CorvajaZannier.ratFuncMinpoly u hu v)

noncomputable def BGS.CorvajaZannier.primitiveClearedMinpolyRelation {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) : Polynomial (Polynomial K)

The primitive bivariate relation obtained from the minimal polynomial of v over K(u).

Equations

• BGS.CorvajaZannier.primitiveClearedMinpolyRelation u hu v = (BGS.CorvajaZannier.integerClearedMinpoly u hu v).primPart

theorem BGS.CorvajaZannier.ratFuncMinpoly_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : ratFuncMinpoly u hu v ≠ 0

theorem BGS.CorvajaZannier.ratFuncMinpoly_irreducible {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : Irreducible (ratFuncMinpoly u hu v)

theorem BGS.CorvajaZannier.integerClearedMinpoly_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : integerClearedMinpoly u hu v ≠ 0

theorem BGS.CorvajaZannier.primitiveClearedMinpolyRelation_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) : primitiveClearedMinpolyRelation u hu v ≠ 0

theorem BGS.CorvajaZannier.primitiveClearedMinpolyRelation_natDegree {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : (primitiveClearedMinpolyRelation u hu v).natDegree = (minpoly (↥K⟮u⟯) v).natDegree

theorem BGS.CorvajaZannier.map_primitiveClearedMinpolyRelation_eq_C_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : ∃ (c : RatFunc K), c ≠ 0 ∧ Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (primitiveClearedMinpolyRelation u hu v) = Polynomial.C c * ratFuncMinpoly u hu v

After embedding the coefficient ring in K(X), the primitive cleared relation is a nonzero constant multiple of the transported minimal polynomial.

theorem BGS.CorvajaZannier.primitiveClearedMinpolyRelation_irreducible {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : Irreducible (primitiveClearedMinpolyRelation u hu v)

The cleared minimal-polynomial relation is irreducible in K[U,V].

noncomputable def BGS.CorvajaZannier.ratFuncSpecialization {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) : RatFunc K →+* L

Specialize the rational-function variable X at a transcendental element u, then include K(u) in the ambient field.

Equations

• BGS.CorvajaZannier.ratFuncSpecialization u hu = (algebraMap (↥K⟮u⟯) L).comp (RatFunc.algEquivOfTranscendental u hu).toRingEquiv.toRingHom

theorem BGS.CorvajaZannier.ratFuncSpecialization_comp_polynomial_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) : (ratFuncSpecialization u hu).comp (algebraMap (Polynomial K) (RatFunc K)) = Polynomial.eval₂RingHom (algebraMap K L) u

theorem BGS.CorvajaZannier.ratFuncSpecialization_comp_symm_algEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) : (ratFuncSpecialization u hu).comp (RatFunc.algEquivOfTranscendental u hu).symm.toRingEquiv.toRingHom = algebraMap (↥K⟮u⟯) L

theorem BGS.CorvajaZannier.evalBivariate_eq_eval₂_ratFuncSpecialization_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (P : Polynomial (Polynomial K)) : evalBivariate u v P = Polynomial.eval₂ (ratFuncSpecialization u hu) v (Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) P)

Evaluation of an iterated polynomial at (u,v) agrees with first mapping its coefficient polynomials to K(X) and then specializing X at u.

theorem BGS.CorvajaZannier.eval₂_ratFuncSpecialization_ratFuncMinpoly_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) : Polynomial.eval₂ (ratFuncSpecialization u hu) v (ratFuncMinpoly u hu v) = 0

The transported minimal polynomial vanishes after specializing the rational-function variable at u and the outer variable at v.

theorem BGS.CorvajaZannier.evalBivariate_primitiveClearedMinpolyRelation_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) : evalBivariate u v (primitiveClearedMinpolyRelation u hu v) = 0

The primitive cleared relation really vanishes at (u,v).

theorem BGS.CorvajaZannier.irreducible_transposeBivariate {K : Type u_1} [Field K] {P : Polynomial (Polynomial K)} (hP : Irreducible P) : Irreducible (transposeBivariate P)

Swapping the two variables preserves irreducibility.

theorem BGS.CorvajaZannier.transposeBivariate_natDegree_ne_zero_of_eval_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u v : L) (hv : Transcendental K v) {P : Polynomial (Polynomial K)} (hP : Irreducible P) (hzero : evalBivariate u v P = 0) : (transposeBivariate P).natDegree ≠ 0

An irreducible relation vanishing at a pair whose first coordinate is transcendental must genuinely depend on its outer variable. Applied after swapping, this says the original relation genuinely depends on its inner variable.

theorem BGS.CorvajaZannier.transposeBivariate_natDegree_eq_minpoly {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (u v : L) (hvTrans : Transcendental K v) {P : Polynomial (Polynomial K)} (hP : Irreducible P) (hzero : evalBivariate u v P = 0) : (transposeBivariate P).natDegree = (minpoly (↥K⟮v⟯) u).natDegree

For an irreducible bivariate relation at a transcendental pair, the degree in the first coordinate is exactly the minimal-polynomial degree over the rational field generated by the second coordinate.

Powered coordinate fields of a plane curve

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.FirstPoweredCoordinateSubfield {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m : ℕ) : IntermediateField K (PlaneCurveFunctionField f)

The rational subfield generated by the powered first coordinate.

Equations

• BGS.CorvajaZannier.FirstPoweredCoordinateSubfield f m = K⟮BGS.CorvajaZannier.planeCurveFunction f 0 ^ m⟯

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.SecondPoweredCoordinateSubfield {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (n : ℕ) : IntermediateField K (PlaneCurveFunctionField f)

The rational subfield generated by the powered second coordinate.

Equations

• BGS.CorvajaZannier.SecondPoweredCoordinateSubfield f n = K⟮BGS.CorvajaZannier.planeCurveFunction f 1 ^ n⟯

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.PoweredCoordinateImageField {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : IntermediateField K (PlaneCurveFunctionField f)

The function field of the image of the powered-coordinate map, realized inside the source function field.

Equations

• BGS.CorvajaZannier.PoweredCoordinateImageField f m n = K⟮BGS.CorvajaZannier.planeCurveFunction f 0 ^ m, BGS.CorvajaZannier.planeCurveFunction f 1 ^ n⟯

theorem BGS.CorvajaZannier.firstPoweredCoordinate_transcendental {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) : Transcendental K (planeCurveFunction f 0 ^ m)

A positive power of the first coordinate remains transcendental.

theorem BGS.CorvajaZannier.secondPoweredCoordinate_transcendental {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : 0 < n) : Transcendental K (planeCurveFunction f 1 ^ n)

A positive power of the second coordinate remains transcendental.

noncomputable def BGS.CorvajaZannier.poweredCoordinateImageRelation {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : Polynomial (Polynomial K)

The canonical irreducible equation of the powered-coordinate image, obtained by clearing the minimal polynomial over K(x^m). The outer variable is the powered second coordinate.

Equations

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

theorem BGS.CorvajaZannier.finiteDimensional_over_firstPoweredCoordinate {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) : FiniteDimensional (↥(FirstPoweredCoordinateSubfield f m)) (PlaneCurveFunctionField f)

The source function field is finite over the field generated by a positive power of its first coordinate.

theorem BGS.CorvajaZannier.finrank_over_firstPoweredCoordinate_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) : Module.finrank (↥(FirstPoweredCoordinateSubfield f m)) (PlaneCurveFunctionField f) ≤ m * MvPolynomial.degreeOf 1 f

Raising the first coordinate to the m-th power multiplies the source degree bound by at most m.

theorem BGS.CorvajaZannier.finiteDimensional_over_secondPoweredCoordinate {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : 0 < n) : FiniteDimensional (↥(SecondPoweredCoordinateSubfield f n)) (PlaneCurveFunctionField f)

The source function field is finite over the field generated by a positive power of its second coordinate.

theorem BGS.CorvajaZannier.finrank_over_secondPoweredCoordinate_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : 0 < n) : Module.finrank (↥(SecondPoweredCoordinateSubfield f n)) (PlaneCurveFunctionField f) ≤ n * MvPolynomial.degreeOf 0 f

Raising the second coordinate to the n-th power multiplies the source degree bound by at most n.

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.PoweredImageOverFirst {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : IntermediateField (↥(FirstPoweredCoordinateSubfield f m)) (PlaneCurveFunctionField f)

The powered image field, presented as an extension of the powered first coordinate field by the powered second coordinate.

Equations

• BGS.CorvajaZannier.PoweredImageOverFirst f m n = (↥(BGS.CorvajaZannier.FirstPoweredCoordinateSubfield f m))⟮BGS.CorvajaZannier.planeCurveFunction f 1 ^ n⟯

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.PoweredImageOverSecond {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : IntermediateField (↥(SecondPoweredCoordinateSubfield f n)) (PlaneCurveFunctionField f)

The powered image field, presented as an extension of the powered second coordinate field by the powered first coordinate.

Equations

• BGS.CorvajaZannier.PoweredImageOverSecond f m n = (↥(BGS.CorvajaZannier.SecondPoweredCoordinateSubfield f n))⟮BGS.CorvajaZannier.planeCurveFunction f 0 ^ m⟯

theorem BGS.CorvajaZannier.restrictScalars_poweredImageOverFirst_eq {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : IntermediateField.restrictScalars K (PoweredImageOverFirst f m n) = PoweredCoordinateImageField f m n

Forgetting the relative base field identifies the first presentation with K(x^m,y^n).

theorem BGS.CorvajaZannier.restrictScalars_poweredImageOverSecond_eq {K : Type u_3} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m n : ℕ) : IntermediateField.restrictScalars K (PoweredImageOverSecond f m n) = PoweredCoordinateImageField f m n

Forgetting the relative base field identifies the second presentation with K(x^m,y^n).

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) : Module.finrank ↥(FirstPoweredCoordinateSubfield f m) ↥(PoweredImageOverFirst f m n) ≤ m * MvPolynomial.degreeOf 1 f

The degree of the powered image over K(x^m) is bounded by the source degree over that same rational subfield.

theorem BGS.CorvajaZannier.finrank_poweredImageOverSecond_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (m n : ℕ) (hn : 0 < n) : Module.finrank ↥(SecondPoweredCoordinateSubfield f n) ↥(PoweredImageOverSecond f m n) ≤ n * MvPolynomial.degreeOf 0 f

The degree of the powered image over K(y^n) is bounded by the source degree over that same rational subfield.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_irreducible {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : Irreducible (poweredCoordinateImageRelation hf hpartialSecond m hm n)

The canonical powered-image equation is irreducible over K.

theorem BGS.CorvajaZannier.evalBivariate_poweredCoordinateImageRelation_eq_zero {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : evalBivariate (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) (poweredCoordinateImageRelation hf hpartialSecond m hm n) = 0

The canonical equation vanishes on the powered coordinate pair.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_natDegree_eq_finrank {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree = Module.finrank ↥(FirstPoweredCoordinateSubfield f m) ↥(PoweredImageOverFirst f m n)

The degree in the powered second coordinate is exactly the projection degree of the image over K(x^m).

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_transpose_natDegree_eq_finrank {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) (hn : 0 < n) : (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree = Module.finrank ↥(SecondPoweredCoordinateSubfield f n) ↥(PoweredImageOverSecond f m n)

The degree in the powered first coordinate is exactly the projection degree of the image over K(y^n).

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_bidegree_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) (hn : 0 < n) : (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree ≤ m * MvPolynomial.degreeOf 1 f ∧ (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree ≤ n * MvPolynomial.degreeOf 0 f

Source-degree bounds for both coordinate degrees of the actual powered image equation.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_coeff_natDegree_le {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n i : ℕ) : ((poweredCoordinateImageRelation hf hpartialSecond m hm n).coeff i).natDegree ≤ (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree

Every coefficient of the canonical powered-image equation has degree at most its first-coordinate degree.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_natDegree_pos {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : 0 < (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree

The canonical powered-image equation has positive degree in the powered second coordinate.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_transpose_natDegree_pos {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) (hn : 0 < n) : 0 < (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree

The canonical powered-image equation has positive degree in the powered first coordinate.

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_spec {K : Type u_3} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) (hn : 0 < n) : have g := poweredCoordinateImageRelation hf hpartialSecond m hm n; Irreducible g ∧ evalBivariate (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) g = 0 ∧ 0 < g.natDegree ∧ 0 < (transposeBivariate g).natDegree ∧ g.natDegree ≤ m * MvPolynomial.degreeOf 1 f ∧ (transposeBivariate g).natDegree ≤ n * MvPolynomial.degreeOf 0 f ∧ ∀ (i : ℕ), (g.coeff i).natDegree ≤ n * MvPolynomial.degreeOf 0 f

A single endpoint collecting the algebraic geometry of the powered coordinate image: an irreducible equation over K, its vanishing, positive bidegrees, source-degree bounds, and the corresponding coefficient bound.