The genus of a smooth plane curve

Let g ∈ k[X, Y] be irreducible of total degree n, with the coefficient of Yⁿ equal to 1, such that the projective closure of g = 0 is smooth in both affine charts g = 0 and uⁿ g(1 / u, v / u) = 0, and let F / k(x) be finite separable, generated by y with g(x, y) = 0. Then deg Diff(F / k(x)) = n (n - 1) (TauCeti.Divisor.degree_different_eq_totalDegree_mul) and [F : k(x)] = n. When k is the exact constant field of F, the Hurwitz genus formula 2g - 2 = -2n + deg Diff(F / k(x)) gives the genus of a smooth plane curve of degree n:

g = (n - 1)(n - 2) / 2.

Main results

• TauCeti.two_mul_genus_eq_of_aeval_eq_zero and TauCeti.genus_eq_of_aeval_eq_zero: the genus of a smooth plane curve of degree n is (n - 1)(n - 2) / 2.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.4.14.
• W. Fulton, Algebraic Curves, Section 8.3, for the genus (n - 1)(n - 2) / 2 of a smooth plane curve of degree n.

theorem TauCeti.two_mul_genus_eq_of_aeval_eq_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] [Algebra.IsSeparable (RatFunc k) F] [FiniteDimensional (RatFunc k) F] (hex : IsIntegrallyClosedIn k F) {g : MvPolynomial (Fin 2) k} (hirr : Irreducible g) (hlead : g.coeff (Finsupp.single 1 g.totalDegree) = 1) (hsm : Ideal.span {g, (MvPolynomial.pderiv 0) g, (MvPolynomial.pderiv 1) g} = ⊤) (hsm' : Ideal.span {MvPolynomial.inftyChart g.totalDegree g, (MvPolynomial.pderiv 0) (MvPolynomial.inftyChart g.totalDegree g), (MvPolynomial.pderiv 1) (MvPolynomial.inftyChart g.totalDegree g)} = ⊤) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (MvPolynomial.aeval ![(algebraMap (RatFunc k) F) RatFunc.X, y]) g = 0) : 2 * ↑(genus k F) = (↑g.totalDegree - 1) * (↑g.totalDegree - 2)

The genus of a smooth plane curve, doubled: under the hypotheses of TauCeti.Divisor.different_eq_principal_add_zsmul_poles, if k is the exact constant field of F, then a smooth plane curve of degree n has 2g = (n - 1)(n - 2).

theorem TauCeti.genus_eq_of_aeval_eq_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] [Algebra.IsSeparable (RatFunc k) F] [FiniteDimensional (RatFunc k) F] (hex : IsIntegrallyClosedIn k F) {g : MvPolynomial (Fin 2) k} (hirr : Irreducible g) (hlead : g.coeff (Finsupp.single 1 g.totalDegree) = 1) (hsm : Ideal.span {g, (MvPolynomial.pderiv 0) g, (MvPolynomial.pderiv 1) g} = ⊤) (hsm' : Ideal.span {MvPolynomial.inftyChart g.totalDegree g, (MvPolynomial.pderiv 0) (MvPolynomial.inftyChart g.totalDegree g), (MvPolynomial.pderiv 1) (MvPolynomial.inftyChart g.totalDegree g)} = ⊤) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (MvPolynomial.aeval ![(algebraMap (RatFunc k) F) RatFunc.X, y]) g = 0) : genus k F = (g.totalDegree - 1) * (g.totalDegree - 2) / 2

The genus of a smooth plane curve (Fulton, Section 8.3): let k be the exact constant field of F, let g ∈ k[X, Y] be irreducible of total degree n, with the coefficient of Yⁿ equal to 1, such that the projective closure of g = 0 is smooth in both affine charts g = 0 and uⁿ g(1 / u, v / u) = 0, and let F / k(x) be finite separable, generated by y with g(x, y) = 0. Then F has genus (n - 1)(n - 2) / 2.