Separability of a plane-curve coordinate extension

For an irreducible plane equation whose partial derivative in the second coordinate is nonzero, this file proves that the function field is a finite separable extension of the field generated by the first coordinate. The proof passes through the iterated-polynomial presentation and Gauss's lemma.

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

The iterated-polynomial presentation of an irreducible bivariate polynomial is irreducible.

theorem BGS.CorvajaZannier.derivative_polynomialInSecondCoordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial.derivative (polynomialInSecondCoordinate f) = polynomialInSecondCoordinate ((MvPolynomial.pderiv 1) f)

Ordinary differentiation of the iterated-polynomial presentation agrees with taking the partial derivative in the second affine coordinate.

theorem BGS.CorvajaZannier.derivative_polynomialInSecondCoordinate_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : Polynomial.derivative (polynomialInSecondCoordinate f) ≠ 0

A nonzero second-coordinate partial derivative remains nonzero after rewriting the equation as a polynomial in the second coordinate over the first-coordinate polynomial ring.

noncomputable def BGS.CorvajaZannier.firstCoordinateFractionEquiv {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (htrans : Transcendental K (planeCurveFunction f 0)) : FractionRing (MvPolynomial { i : Fin 2 // i ≠ 1 } K) ≃ₐ[K] ↥(FirstCoordinateSubfield f)

The fraction field of the polynomial coefficient ring in the remaining affine coordinate is the intermediate field generated by the first coordinate function.

Equations

• BGS.CorvajaZannier.firstCoordinateFractionEquiv f htrans = ⋯.aevalEquivField.trans (IntermediateField.equivOfEq ⋯)

@[simp]

theorem BGS.CorvajaZannier.firstCoordinateFractionEquiv_algebraMap {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (htrans : Transcendental K (planeCurveFunction f 0)) (p : MvPolynomial { i : Fin 2 // i ≠ 1 } K) : (firstCoordinateFractionEquiv f htrans) ((algebraMap (MvPolynomial { i : Fin 2 // i ≠ 1 } K) (FractionRing (MvPolynomial { i : Fin 2 // i ≠ 1 } K))) p) = (firstCoordinateCoefficientEval f) p

The fraction-field equivalence extends the coefficient evaluation homomorphism.

theorem BGS.CorvajaZannier.polynomialOverFirstCoordinate_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : Irreducible (polynomialOverFirstCoordinate f)

An irreducible plane equation with nonzero second partial derivative stays irreducible after passing to the field generated by the first coordinate and viewing it as a polynomial in the second coordinate.

theorem BGS.CorvajaZannier.derivative_polynomialOverFirstCoordinate_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : Polynomial.derivative (polynomialOverFirstCoordinate f) ≠ 0

The ordinary derivative of the specialized plane equation is nonzero.

theorem BGS.CorvajaZannier.polynomialOverFirstCoordinate_separable {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : (polynomialOverFirstCoordinate f).Separable

The specialized defining polynomial over the first-coordinate field is separable.

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

The second coordinate function is separable over the field generated by the first coordinate.

theorem BGS.CorvajaZannier.finiteSeparable_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) ∧ Algebra.IsSeparable (↥(FirstCoordinateSubfield f)) (PlaneCurveFunctionField f)

The plane-curve function field is a finite separable extension of the field generated by its first coordinate.

theorem BGS.CorvajaZannier.natDegree_polynomialOverFirstCoordinate_eq_degreeOf_second {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : (polynomialOverFirstCoordinate f).natDegree = MvPolynomial.degreeOf 1 f

Specialization at the transcendental first coordinate preserves the second-coordinate degree.

theorem BGS.CorvajaZannier.natDegree_minpoly_secondCoordinate_eq_degreeOf_second {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 1) f ≠ 0) : (minpoly (↥(FirstCoordinateSubfield f)) (planeCurveFunction f 1)).natDegree = MvPolynomial.degreeOf 1 f

The minimal polynomial of the second coordinate has the full second-coordinate degree of the irreducible plane equation.

theorem BGS.CorvajaZannier.finrank_over_firstCoordinate_eq_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 extension degree over the first-coordinate field is exactly the degree of the defining equation in the second coordinate.

The coordinate-swapped extension

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

Embed a univariate polynomial in the second affine coordinate.

Equations

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

theorem BGS.CorvajaZannier.eval₂_polynomialInSecondCoordinateOnly {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] (polynomialInSecondCoordinateOnly P) = Polynomial.eval₂ phi y P

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

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

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

Positive degree in the first coordinate makes the second coordinate function transcendental.

@[reducible, inline]

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

The intermediate field generated by the second coordinate function.

Equations

• BGS.CorvajaZannier.SecondCoordinateSubfield f = K⟮BGS.CorvajaZannier.planeCurveFunction f 1⟯

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

The second coordinate viewed in the coefficient subfield of the plane curve.

Equations

• BGS.CorvajaZannier.secondCoordinateInSubfield f = ⟨BGS.CorvajaZannier.planeCurveFunction f 1, ⋯⟩

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

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

Equations

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

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

Iterated-polynomial presentation with the original first coordinate as outer variable.

Equations

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

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

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

Evaluation of a coefficient polynomial at the second coordinate.

Equations

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

theorem BGS.CorvajaZannier.secondCoordinateCoefficientEval_injective {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hfirst : 0 < MvPolynomial.degreeOf 0 f) : Function.Injective ⇑(secondCoordinateCoefficientEval f)

theorem BGS.CorvajaZannier.polynomialOverSecondCoordinate_eq_map_polynomialInFirstVariablePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : polynomialOverSecondCoordinate f = Polynomial.map (secondCoordinateCoefficientEval f) (polynomialInFirstVariablePresentation f)

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

theorem BGS.CorvajaZannier.derivative_polynomialInFirstVariablePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial.derivative (polynomialInFirstVariablePresentation f) = polynomialInFirstVariablePresentation ((MvPolynomial.pderiv 0) f)

theorem BGS.CorvajaZannier.derivative_polynomialInFirstVariablePresentation_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : Polynomial.derivative (polynomialInFirstVariablePresentation f) ≠ 0

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

theorem BGS.CorvajaZannier.polynomialOverSecondCoordinate_ne_zero_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hfirst : 0 < MvPolynomial.degreeOf 0 f) : polynomialOverSecondCoordinate f ≠ 0

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

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

theorem BGS.CorvajaZannier.firstCoordinate_isAlgebraic_over_second {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (hpoly : polynomialOverSecondCoordinate f ≠ 0) : IsAlgebraic (↥(SecondCoordinateSubfield f)) (planeCurveFunction f 0)

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

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

noncomputable def BGS.CorvajaZannier.secondCoordinateFractionEquiv {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (htrans : Transcendental K (planeCurveFunction f 1)) : FractionRing (MvPolynomial { i : Fin 2 // i ≠ 0 } K) ≃ₐ[K] ↥(SecondCoordinateSubfield f)

The fraction field of the coefficient polynomial ring in the second affine coordinate is the field generated by that coordinate function.

Equations

• BGS.CorvajaZannier.secondCoordinateFractionEquiv f htrans = ⋯.aevalEquivField.trans (IntermediateField.equivOfEq ⋯)

@[simp]

theorem BGS.CorvajaZannier.secondCoordinateFractionEquiv_algebraMap {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (htrans : Transcendental K (planeCurveFunction f 1)) (p : MvPolynomial { i : Fin 2 // i ≠ 0 } K) : (secondCoordinateFractionEquiv f htrans) ((algebraMap (MvPolynomial { i : Fin 2 // i ≠ 0 } K) (FractionRing (MvPolynomial { i : Fin 2 // i ≠ 0 } K))) p) = (secondCoordinateCoefficientEval f) p

The second-coordinate fraction-field equivalence extends coefficient evaluation.

theorem BGS.CorvajaZannier.polynomialOverSecondCoordinate_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : Irreducible (polynomialOverSecondCoordinate f)

The plane equation remains irreducible over the field generated by the second coordinate when viewed as a polynomial in the first coordinate.

theorem BGS.CorvajaZannier.derivative_polynomialOverSecondCoordinate_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : Polynomial.derivative (polynomialOverSecondCoordinate f) ≠ 0

theorem BGS.CorvajaZannier.polynomialOverSecondCoordinate_separable {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : (polynomialOverSecondCoordinate f).Separable

theorem BGS.CorvajaZannier.firstCoordinate_isSeparable_over_second {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : IsSeparable (↥(SecondCoordinateSubfield f)) (planeCurveFunction f 0)

The first coordinate is separable over the field generated by the second coordinate.

theorem BGS.CorvajaZannier.finiteSeparable_over_secondCoordinate_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : FiniteDimensional (↥(SecondCoordinateSubfield f)) (PlaneCurveFunctionField f) ∧ Algebra.IsSeparable (↥(SecondCoordinateSubfield f)) (PlaneCurveFunctionField f)

The plane-curve function field is finite and separable over the field generated by its second coordinate.

theorem BGS.CorvajaZannier.natDegree_polynomialOverSecondCoordinate_eq_degreeOf_first {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : (polynomialOverSecondCoordinate f).natDegree = MvPolynomial.degreeOf 0 f

theorem BGS.CorvajaZannier.natDegree_minpoly_firstCoordinate_eq_degreeOf_first {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hderiv : (MvPolynomial.pderiv 0) f ≠ 0) : (minpoly (↥(SecondCoordinateSubfield f)) (planeCurveFunction f 0)).natDegree = MvPolynomial.degreeOf 0 f

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

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