Constants in an absolutely irreducible plane-curve function field

This file develops the constant-field step needed by the function-field Bombieri--Stepanov proof of Hasse--Weil. The key algebraic point is that, after enlarging the constants inside the original function field, the base-changed plane equation is still the primitive cleared minimal relation of the second coordinate over the first-coordinate rational subfield.

No geometric Hasse--Weil statement is assumed here.

theorem BGS.HasseWeil.evalBivariate_planeCurveToBivariate {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (x y : L) : CorvajaZannier.evalBivariate y x ((CorvajaZannier.planeCurveToBivariate K) f) = MvPolynomial.eval₂ (algebraMap K L) ![x, y] f

The iterated-polynomial presentation evaluates at the same ordered pair as the original bivariate polynomial.

noncomputable def BGS.HasseWeil.planeCurveSecondOuterRelation (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial (Polynomial K)

Swap the iterated presentation so that the second affine coordinate is the outer polynomial variable.

Equations

• BGS.HasseWeil.planeCurveSecondOuterRelation K f = BGS.CorvajaZannier.transposeBivariate ((BGS.CorvajaZannier.planeCurveToBivariate K) f)

theorem BGS.HasseWeil.evalBivariate_planeCurveSecondOuterRelation {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (x y : L) : CorvajaZannier.evalBivariate x y (planeCurveSecondOuterRelation K f) = MvPolynomial.eval₂ (algebraMap K L) ![x, y] f

theorem BGS.HasseWeil.planeCurveSecondOuterRelation_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) : Irreducible (planeCurveSecondOuterRelation K f)

Irreducibility is preserved by the two variable-presentation equivalences.

theorem BGS.HasseWeil.planeCurveSecondOuterRelation_natDegree (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : (planeCurveSecondOuterRelation K f).natDegree = MvPolynomial.degreeOf 1 f

The outer degree in the swapped presentation is exactly the degree in the second affine coordinate.

theorem BGS.HasseWeil.primitiveClearedMinpolyRelation_associated_planeRelation {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (x y : L) (hx : Transcendental K x) (hy : IsIntegral (↥K⟮x⟯) y) (hzero : MvPolynomial.eval₂ (algebraMap K L) ![x, y] f = 0) : Associated (CorvajaZannier.primitiveClearedMinpolyRelation x hx y) (planeCurveSecondOuterRelation K f)

Over any enlarged constant field inside the ambient function field, an irreducible plane equation is associated to the primitive cleared minimal relation of the second coordinate.

theorem BGS.HasseWeil.minpoly_natDegree_eq_planeRelation_secondDegree {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (x y : L) (hx : Transcendental K x) (hy : IsIntegral (↥K⟮x⟯) y) (hzero : MvPolynomial.eval₂ (algebraMap K L) ![x, y] f = 0) : (minpoly (↥K⟮x⟯) y).natDegree = MvPolynomial.degreeOf 1 f

Consequently the minimal-polynomial degree over K(x) is the second coordinate degree of the irreducible plane relation.

theorem BGS.HasseWeil.ratFunc_algebraicClosure_eq_bot (K : Type u_1) [Field K] : algebraicClosure K (RatFunc K) = ⊥

A rational function field has no constants algebraic over its coefficient field beyond the coefficient field itself. Lüroth's theorem makes this a short argument: any nontrivial intermediate field has a transcendental generator, whereas every element of the relative algebraic closure is algebraic.

theorem BGS.HasseWeil.adjoin_transcendental_algebraicClosure_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) (hx : Transcendental K x) : algebraicClosure K ↥K⟮x⟯ = ⊥

The field generated by one transcendental element has the same exact constant field as a rational function field.

theorem BGS.HasseWeil.planeCurveFunctionField_algebraicClosure_eq_bot {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hf := ⋯; have x := ⋯; algebraicClosure K (CorvajaZannier.PlaneCurveFunctionField f) = ⊥

Exact constant field of an absolutely irreducible plane curve.

If the defining equation remains irreducible over an algebraic closure and the second coordinate is separating, then the only elements of its function field algebraic over K are the elements of K itself.

The proof compares the degree over K(x) with the degree after adjoining the relative algebraic closure E to the constants. Absolute irreducibility and the cleared-minimal-polynomial relation show that both degrees are exactly degreeOf 1 f. The tower formula therefore forces E(x) = K(x). Finally, the rational-function constant-field theorem above forces every element of E back into K.

theorem BGS.HasseWeil.planeCurveBaseChangeFunctionField_algebraicClosure_eq_bot {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : let fE := (MvPolynomial.map (algebraMap K E)) f; have hfE := ⋯; algebraicClosure E (CorvajaZannier.PlaneCurveFunctionField fE) = ⊥

Exact constants persist after an arbitrary extension of the coefficient field. Absolute irreducibility over K supplies absolute irreducibility over E, and injectivity of the coefficient embedding preserves the separating second partial derivative.