Function fields of irreducible affine plane curves

This file constructs the affine coordinate domain and its fraction field directly from an irreducible polynomial in two variables. It also records the two coordinate functions and their defining relation. These are the algebraic objects used in the plane-curve specialization of the Corvaja--Zannier argument.

@[reducible, inline]

abbrev BGS.CorvajaZannier.PlaneCurveCoordinateRing {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Type u_1

The affine coordinate ring of the plane curve cut out by f.

Equations

• BGS.CorvajaZannier.PlaneCurveCoordinateRing f = (MvPolynomial (Fin 2) K ⧸ Ideal.span {f})

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.planeCurveQuotientMap {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : MvPolynomial (Fin 2) K →+* PlaneCurveCoordinateRing f

The quotient map from the polynomial ring to the affine coordinate ring.

Equations

• BGS.CorvajaZannier.planeCurveQuotientMap f = Ideal.Quotient.mk (Ideal.span {f})

noncomputable def BGS.CorvajaZannier.planeCurveCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (i : Fin 2) : PlaneCurveCoordinateRing f

The two affine coordinate classes in the coordinate ring.

Equations

• BGS.CorvajaZannier.planeCurveCoordinate f i = (BGS.CorvajaZannier.planeCurveQuotientMap f) (MvPolynomial.X i)

theorem BGS.CorvajaZannier.eval₂_planeCurveCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : MvPolynomial.eval₂Hom (algebraMap K (PlaneCurveCoordinateRing f)) (planeCurveCoordinate f) = planeCurveQuotientMap f

Evaluation at the coordinate classes is the quotient map.

theorem BGS.CorvajaZannier.eval₂_planeCurveCoordinate_eq_zero {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : MvPolynomial.eval₂ (algebraMap K (PlaneCurveCoordinateRing f)) (planeCurveCoordinate f) f = 0

The coordinate classes satisfy the equation defining the curve.

theorem BGS.CorvajaZannier.planeCurveCoordinateRing_isDomain {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) : IsDomain (PlaneCurveCoordinateRing f)

Irreducibility of the equation makes its affine coordinate ring a domain.

@[reducible, inline]

abbrev BGS.CorvajaZannier.PlaneCurveFunctionField {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Type u_1

The rational function field of the affine plane curve.

Equations

• BGS.CorvajaZannier.PlaneCurveFunctionField f = FractionRing (BGS.CorvajaZannier.PlaneCurveCoordinateRing f)

noncomputable def BGS.CorvajaZannier.planeCurveFunction {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (i : Fin 2) : PlaneCurveFunctionField f

A coordinate function in the fraction field of the curve.

Equations

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

theorem BGS.CorvajaZannier.eval₂_planeCurveFunction {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : MvPolynomial.eval₂Hom (algebraMap K (PlaneCurveFunctionField f)) (planeCurveFunction f) = (algebraMap (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)).comp (planeCurveQuotientMap f)

The quotient map followed by passage to the fraction field is evaluation at the two coordinate functions.

theorem BGS.CorvajaZannier.eval₂_planeCurveFunction_eq_zero {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : MvPolynomial.eval₂ (algebraMap K (PlaneCurveFunctionField f)) (planeCurveFunction f) f = 0

The two rational coordinate functions satisfy the equation of the curve.

theorem BGS.CorvajaZannier.algebraMap_coordinateRing_mem_adjoin_coordinates {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] (a : PlaneCurveCoordinateRing f) : (algebraMap (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)) a ∈ IntermediateField.adjoin K (Set.range (planeCurveFunction f))

Every affine regular function, viewed in the fraction field, belongs to the field generated by the two coordinate functions.

theorem BGS.CorvajaZannier.adjoin_planeCurveFunctions_eq_top {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] : IntermediateField.adjoin K (Set.range (planeCurveFunction f)) = ⊤

The fraction field is generated, as a field over K, by its two coordinate functions.

theorem BGS.CorvajaZannier.adjoin_planeCurveFunctions_eq_top_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) : IntermediateField.adjoin K (Set.range (planeCurveFunction f)) = ⊤

Irreducibility supplies the domain instance needed by adjoin_planeCurveFunctions_eq_top.

noncomputable def BGS.CorvajaZannier.polynomialInFirstCoordinate {K : Type u_1} [Field K] (P : Polynomial K) : MvPolynomial (Fin 2) K

Embed a univariate polynomial in the first coordinate of the affine plane.

Equations

• BGS.CorvajaZannier.polynomialInFirstCoordinate P = P.sum fun (n : ℕ) (c : K) => MvPolynomial.C c * MvPolynomial.X 0 ^ n

theorem BGS.CorvajaZannier.eval₂_polynomialInFirstCoordinate {K : Type u_1} [Field K] {S : Type u_2} [CommSemiring S] (P : Polynomial K) (phi : K →+* S) (x y : S) : MvPolynomial.eval₂ phi ![x, y] (polynomialInFirstCoordinate P) = Polynomial.eval₂ phi x P

Evaluating a polynomial embedded in the first coordinate is ordinary univariate evaluation.

theorem BGS.CorvajaZannier.polynomialInFirstCoordinate_ne_zero {K : Type u_1} [Field K] {P : Polynomial K} (hP : P ≠ 0) : polynomialInFirstCoordinate P ≠ 0

The embedding in the first coordinate is injective.

theorem BGS.CorvajaZannier.polynomialInFirstCoordinate_degreeOf_second_le {K : Type u_1} [Field K] (P : Polynomial K) : MvPolynomial.degreeOf 1 (polynomialInFirstCoordinate P) ≤ 0

A polynomial embedded in the first coordinate has degree zero in the second coordinate.

theorem BGS.CorvajaZannier.firstCoordinate_transcendental {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) : Transcendental K (planeCurveFunction f 0)

On an irreducible plane curve of positive second-coordinate degree, the first coordinate function is transcendental over the constant field.

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.FirstCoordinateSubfield {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : IntermediateField K (PlaneCurveFunctionField f)

The intermediate field generated by the first coordinate function.

Equations

• BGS.CorvajaZannier.FirstCoordinateSubfield f = K⟮BGS.CorvajaZannier.planeCurveFunction f 0⟯

noncomputable def BGS.CorvajaZannier.firstCoordinateInSubfield {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : ↥(FirstCoordinateSubfield f)

The first coordinate function, regarded as an element of its generated subfield.

Equations

• BGS.CorvajaZannier.firstCoordinateInSubfield f = ⟨BGS.CorvajaZannier.planeCurveFunction f 0, ⋯⟩

noncomputable def BGS.CorvajaZannier.polynomialOverFirstCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : Polynomial ↥(FirstCoordinateSubfield f)

Regard the plane equation as a polynomial in the second coordinate, with coefficients in the field generated by the first coordinate.

Equations

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

noncomputable def BGS.CorvajaZannier.polynomialInSecondCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial (MvPolynomial { i : Fin 2 // i ≠ 1 } K)

The same change of viewpoint before specializing the remaining coefficient variable. The outer polynomial variable is the original second coordinate.

Equations

• BGS.CorvajaZannier.polynomialInSecondCoordinate f = (MvPolynomial.optionEquivLeft K { i : Fin 2 // i ≠ 1 }) ((MvPolynomial.rename ⇑(Equiv.optionSubtypeNe 1).symm) f)

theorem BGS.CorvajaZannier.polynomialInSecondCoordinate_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : f ≠ 0) : polynomialInSecondCoordinate f ≠ 0

The iterated-polynomial presentation preserves nonzeroness.

noncomputable def BGS.CorvajaZannier.firstCoordinateCoefficientEval {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : MvPolynomial { i : Fin 2 // i ≠ 1 } K →+* ↥(FirstCoordinateSubfield f)

Evaluate the sole coefficient variable at the first coordinate function.

Equations

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

theorem BGS.CorvajaZannier.firstCoordinateCoefficientEval_injective {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) : Function.Injective ⇑(firstCoordinateCoefficientEval f)

Positive degree in the second coordinate makes coefficient evaluation at the first coordinate injective.

theorem BGS.CorvajaZannier.polynomialOverFirstCoordinate_eq_map_polynomialInSecondCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : polynomialOverFirstCoordinate f = Polynomial.map (firstCoordinateCoefficientEval f) (polynomialInSecondCoordinate f)

The direct two-variable specialization agrees with the standard MvPolynomial.optionEquivLeft presentation.

theorem BGS.CorvajaZannier.polynomialOverFirstCoordinate_ne_zero_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) : polynomialOverFirstCoordinate f ≠ 0

Irreducibility and positive degree in the second variable ensure that the equation remains nonzero after passing to the field generated by the first coordinate.

theorem BGS.CorvajaZannier.natDegree_polynomialOverFirstCoordinate_le_degreeOf_second {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : (polynomialOverFirstCoordinate f).natDegree ≤ MvPolynomial.degreeOf 1 f

Specializing the coefficient variable cannot increase the degree in the second coordinate.

theorem BGS.CorvajaZannier.eval₂_polynomialOverFirstCoordinate_eq_zero {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : Polynomial.eval₂ (algebraMap (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f)) (planeCurveFunction f 1) (polynomialOverFirstCoordinate f) = 0

Substituting the second coordinate function into polynomialOverFirstCoordinate recovers the defining plane-curve relation.

theorem BGS.CorvajaZannier.secondCoordinate_isAlgebraic_over_first {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hpoly : polynomialOverFirstCoordinate f ≠ 0) : IsAlgebraic (↥(FirstCoordinateSubfield f)) (planeCurveFunction f 1)

If the specialized equation is nonzero, the second coordinate is algebraic over the field generated by the first coordinate.

theorem BGS.CorvajaZannier.range_planeCurveFunction {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Set.range (planeCurveFunction f) = {planeCurveFunction f 0, planeCurveFunction f 1}

The range of the coordinate-function family is exactly the two-element set of affine coordinates.

theorem BGS.CorvajaZannier.adjoin_secondCoordinate_over_first_eq_top {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : (↥(FirstCoordinateSubfield f))⟮planeCurveFunction f 1⟯ = ⊤

After adjoining the first coordinate to K, adjoining the second coordinate generates the entire plane-curve function field.

theorem BGS.CorvajaZannier.finiteDimensional_over_firstCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hpoly : polynomialOverFirstCoordinate f ≠ 0) : FiniteDimensional (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f)

A nonzero specialization of the plane equation makes the function field finite-dimensional over the field generated by the first coordinate.

theorem BGS.CorvajaZannier.finrank_over_firstCoordinate_le_degreeOf_second {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hpoly : polynomialOverFirstCoordinate f ≠ 0) : Module.finrank (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f) ≤ MvPolynomial.degreeOf 1 f

The extension degree over the first-coordinate field is at most the degree of the plane equation in the second coordinate.

theorem BGS.CorvajaZannier.degreeOf_second_pos_of_pderiv_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : 0 < MvPolynomial.degreeOf 1 f

A nonzero partial derivative in the second coordinate forces positive degree in that coordinate.

theorem BGS.CorvajaZannier.finiteDimensional_over_firstCoordinate_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : FiniteDimensional (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f)

For an irreducible plane equation depending on the second coordinate, the function field is finite over the field generated by the first coordinate.

theorem BGS.CorvajaZannier.finrank_over_firstCoordinate_le_degreeOf_second_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : Module.finrank (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f) ≤ MvPolynomial.degreeOf 1 f

The degree of the plane-curve function field over the first-coordinate rational subfield is bounded by the degree of the defining equation in the second coordinate.