The constant field of a plane curve

Let F be a field generated over k by a transcendental element x and an element y with φ(x, y) = 0, for an irreducible φ ∈ k[X, Y]. This file proves the absolute-irreducibility criterion for the constant field: if φ stays irreducible over an algebraically closed field K ⊇ k, then k is algebraically closed in F, that is, k is the exact field of constants of F. This is Stichtenoth's Corollary 3.6.8, stated in his Section 3.6, where k is assumed perfect; the proof here needs no hypothesis on k. It supplies the exactness of constants for function fields given by an absolutely irreducible plane equation.

The exact-constants criterion passes through the tensor product F ⊗[k] K and reuses the domain criterion after converting the bivariate equation to two-variable polynomial form.

• The relations between x and y are exactly the multiples of φ: the kernel of evaluation k[X, Y] → F at (x, y) is the principal ideal (φ). Indeed φ(x, Y) has positive degree in Y, since x is transcendental, so by Gauss's lemma it is irreducible over k(x). It is therefore a multiple of the minimal polynomial of y over k(x) and divides every ψ(x, Y) with ψ(x, y) = 0, first over k(x) and then, again by Gauss's lemma, over k[x].
• So the ring k[x, y] is k[X, Y] / (φ), and since K is flat over k, the ring k[x, y] ⊗[k] K is K[X, Y] / (φ). This is a domain when φ is irreducible, hence prime, in K[X, Y]. Its localization F ⊗[k] K is then a domain as well (TauCeti.isDomain_tensorProduct_of_isLocalization), because F is the fraction field of k[x, y].
• When K is algebraically closed, F ⊗[k] K being a domain forces k to be algebraically closed in F (TauCeti.algebraicClosure_eq_bot_of_isDomain_tensorProduct).

Main results

• TauCeti.ker_aeval_eq_span_singleton_of_irreducible: the ideal of relations of (x, y) over k is generated by φ.
• TauCeti.isDomain_tensorProduct_of_irreducible_map: if φ is irreducible over a field K containing k, then F ⊗[k] K is a domain.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.6.8.

theorem TauCeti.ker_aeval_eq_span_singleton_of_irreducible {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {φ : MvPolynomial (Fin 2) k} (hφ : Irreducible φ) {x y : F} (hx : Transcendental k x) (h : (MvPolynomial.aeval ![x, y]) φ = 0) : RingHom.ker (MvPolynomial.aeval ![x, y]) = Ideal.span {φ}

The relations of a point on a plane curve. If x is transcendental over k and φ(x, y) = 0 for an irreducible φ ∈ k[X, Y], then the polynomials vanishing at (x, y) are exactly the multiples of φ.

theorem TauCeti.isDomain_tensorProduct_of_irreducible_map {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (K : Type u_3) [Field K] [Algebra k K] {φ : MvPolynomial (Fin 2) k} (hφ : Irreducible ((MvPolynomial.map (algebraMap k K)) φ)) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y]) φ = 0) : IsDomain (TensorProduct k F K)

Plane curves stay integral under extension of scalars. Let F be generated over k by a transcendental x and an element y with φ(x, y) = 0. If φ ∈ k[X, Y] is irreducible over a field K containing k, then F ⊗[k] K is a domain.

The absolute-irreducibility criterion

theorem TauCeti.isIntegrallyClosedIn_of_irreducible_map {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {L : Type u_3} [Field L] [Algebra k L] [IsAlgClosed L] {x y : F} (hx : Transcendental k x) (hxy : k⟮x, y⟯ = ⊤) {φ : Polynomial (Polynomial k)} (hφ : Irreducible (Polynomial.map (Polynomial.mapRingHom (algebraMap k L)) φ)) (h : (Polynomial.aevalAeval x y) φ = 0) : IsIntegrallyClosedIn k F

An absolutely irreducible plane equation has exact constants (Stichtenoth, Corollary 3.6.8). Let F = k⟮x, y⟯ with x transcendental over k, and let φ(x, y) = 0 for a polynomial φ ∈ k[X][Y] which stays irreducible over an algebraically closed field L containing k. Then k is the exact constant field of F.

No perfectness of k is needed. Absolute irreducibility is only sufficient: over an imperfect field the constants of F can be exact although φ factors over L, as for y ^ p = t x ^ p + u over 𝔽_p(t, u).