The function field of a plane curve

A field F generated over k by a transcendental element x and a root y of g(x, Y), for a nonzero g ∈ k[X, Y], is an algebraic function field over k: y is algebraic over k(x), so F / k(x) is finite. If moreover ∂g/∂Y (x, y) ≠ 0, then F / k(x) is separable.

Main results

• TauCeti.isFunctionField_of_aeval_eq_zero: a field generated by a transcendental x and a root y of a nonzero g(x, Y) is an algebraic function field.
• TauCeti.finiteDimensional_and_isSeparable_of_aeval_pderiv_one_ne_zero: for any g, if ∂g/∂Y (x, y) ≠ 0, then F / k(x) is finite and separable.

theorem TauCeti.isFunctionField_of_aeval_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {g : MvPolynomial (Fin 2) k} (hg : g ≠ 0) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y]) g = 0) : IsFunctionField k F

The function field of a plane curve: a field generated over k by a transcendental x and a root y of g(x, Y), for a nonzero g ∈ k[X, Y], is an algebraic function field.

theorem TauCeti.finiteDimensional_and_isSeparable_of_aeval_pderiv_one_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] {g : MvPolynomial (Fin 2) k} {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (MvPolynomial.aeval ![(algebraMap (RatFunc k) F) RatFunc.X, y]) g = 0) (hd : (MvPolynomial.aeval ![(algebraMap (RatFunc k) F) RatFunc.X, y]) ((MvPolynomial.pderiv 1) g) ≠ 0) : FiniteDimensional (RatFunc k) F ∧ Algebra.IsSeparable (RatFunc k) F

A plane curve on which ∂g/∂Y does not vanish is separable over k(x): let g ∈ k[X, Y], and let F / k(x) be generated by y with g(x, y) = 0 and ∂g/∂Y (x, y) ≠ 0. Then F / k(x) is finite and separable: y is a simple root of g(x, Y), so its minimal polynomial has nonzero derivative. This is the converse of TauCeti.aeval_pderiv_one_ne_zero_of_aeval_eq_zero.