The genus and the canonical divisors of a smooth projective plane curve

Let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, and suppose the projective curve G = 0 is nonsingular: at every point (b₀ : b₁ : b₂) of G = 0 over an algebraically closed extension K of k, some partial derivative of G is nonzero. Let F / k be generated by x and y with G(x, y, 1) = 0, where x is transcendental. Then

g(F) = (d - 1)(d - 2) / 2.

TauCeti.genus_eq_of_aeval_eq_zero proves this for the projection (x, y) ↦ x from the point (0 : 1 : 0), provided that this point is off the curve, both affine charts are smooth, and F / k(x) is separable. Here the centre of projection is chosen instead. For c ∈ k the shear X₀ ↦ X₀ + c X₁ turns projection from (c : 1 : 0) into projection from (0 : 1 : 0), with the coordinate u = x - c y. Two conditions on c make the theorem applicable:

• (c : 1 : 0) is off the curve, G(c, 1, 0) ≠ 0. The binary form G(X₀, X₁, 0) is nonzero: otherwise the line at infinity X₂ = 0 would be a component of the curve, and the curve would be singular where this line meets the rest of it. So at most d values of c are excluded.
• the projection is separable: c ∂G/∂X₀ + ∂G/∂X₁ does not vanish at (x, y, 1). Since the affine curve is smooth, the two partial derivatives do not vanish together at (x, y, 1), so at most one value of c is excluded.

Nonsingularity is a condition at the points over K; the weak Nullstellensatz turns it into the ideal-theoretic smoothness of the affine charts that TauCeti.genus_eq_of_aeval_eq_zero uses (TauCeti.span_insert_range_pderiv_dehomogenize_eq_top), and the shear preserves it (MvPolynomial.exists_aeval_pderiv_linearSubst_ne_zero). A suitable c exists once k has more than d + 1 elements. A small finite constant field is first enlarged by a finite constant field extension, which preserves the genus. No irreducibility or exactness hypothesis is needed: the affine equation G(X₀, X₁, 1) of a nonsingular projective plane curve is irreducible over K, hence over every intermediate field of K / k (TauCeti.irreducible_map_dehomogenize), and this makes k the exact constant field of F (TauCeti.isIntegrallyClosedIn_of_irreducible_map).

The same projection identifies the canonical class. For nonzero x and y, the line at infinity X₂ = 0 cuts out on the curve the divisor H = (x)_∞ ⊔ (y)_∞, whose coefficient at a place P is the largest pole order of x and y there. Since (c : 1 : 0) is off the curve, y has no worse poles than u, and so H = (u)_∞, which has degree [F : k(u)] = d. Since y has degree d over k(u), the monomials u ^ i y ^ j with i + j < d are linearly independent, and so are the monomials x ^ i y ^ j with i + j < d, which span the same space (TauCeti.span_add_smul_pow_mul_pow). The (d - 1)(d - 2) / 2 = g monomials with i + j ≤ d - 3 lie in L((d - 3) H), a divisor of degree d (d - 3) = 2g - 2, and a divisor of degree 2g - 2 with ℓ ≥ g is canonical (TauCeti.divisorClass_eq_canonicalClass_iff). So for d ≥ 3, the effective canonical divisors of a smooth plane curve of degree d are cut out by the curves of degree d - 3, and the monomials form a basis of L((d - 3) H). For lines and conics (d = 1, 2) there are no curves of negative degree, but the signed formula still holds: (d - 3) H is canonical and L((d - 3) H) = 0. Independence and the degree of H descend from a finite constant field extension when k is small.

Main results

• TauCeti.exists_isSeparable_finrank_eq_of_isHomogeneous_of_lt_card: over a field with more than d + 1 elements, a centre of projection (c : 1 : 0) off a smooth projective plane curve of degree d whose linear coordinate u = x - c y is separating, with [F : k(u)] = d.
• TauCeti.genus_eq_of_isHomogeneous_of_lt_card: the genus (d - 1)(d - 2) / 2 of a smooth projective plane curve of degree d over a field with more than d + 1 elements.
• TauCeti.genus_eq_of_isHomogeneous: the same over every field k.
• TauCeti.isIntegrallyClosedIn_of_isHomogeneous: k is the exact constant field of F.
• TauCeti.genus_eq_of_isHomogeneous_of_aeval_insertNth_eq_zero and TauCeti.isIntegrallyClosedIn_of_isHomogeneous_of_aeval_insertNth_eq_zero: the same two statements for generators x and y read in any of the three affine charts Xᵢ = 1, with either of them transcendental.
• TauCeti.degree_sup_poles_of_isHomogeneous: the line at infinity cuts out a divisor (x)_∞ ⊔ (y)_∞ of degree d.
• TauCeti.linearIndepOn_pow_mul_pow_of_isHomogeneous: the monomials x ^ i y ^ j with i + j < d are linearly independent.
• TauCeti.divisorClass_sub_three_zsmul_sup_poles_eq_canonicalClass_of_isHomogeneous: (d - 3) ((x)_∞ ⊔ (y)_∞) is canonical.
• TauCeti.riemannRochSpace_sub_three_zsmul_sup_poles_eq_span_of_isHomogeneous: L((d - 3) ((x)_∞ ⊔ (y)_∞)) is spanned by the monomials x ^ i y ^ j with i + j ≤ d - 3.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.4.14 and Theorem 3.6.3.
• W. Fulton, Algebraic Curves, Sections 5.1, 8.3 and 8.5.

The line at infinity is not a component of a smooth curve

Choosing the centre of projection

The shear moving the centre of projection to (0 : 1 : 0)

The genus

theorem TauCeti.exists_isSeparable_finrank_eq_of_isHomogeneous_of_lt_card {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) (hcard : ↑(d + 1) < ENat.card k) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : ∃ (c : k), (MvPolynomial.eval ![c, 1, 0]) G ≠ 0 ∧ Transcendental k (x - (algebraMap k F) c * y) ∧ FiniteDimensional (↥k⟮x - (algebraMap k F) c * y⟯) F ∧ Algebra.IsSeparable (↥k⟮x - (algebraMap k F) c * y⟯) F ∧ Module.finrank (↥k⟮x - (algebraMap k F) c * y⟯) F = d

A separating projection of a smooth projective plane curve: let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d with every point of G = 0 over an algebraically closed extension K of k nonsingular, and let F / k be generated by a transcendental x and an element y with G(x, y, 1) = 0. If k has more than d + 1 elements, then some centre of projection (c : 1 : 0) lies off the curve and its linear coordinate u = x - c y is transcendental over k, with F / k(u) finite and separable of degree d.

theorem TauCeti.genus_eq_of_isHomogeneous_of_lt_card {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hex : IsIntegrallyClosedIn k F) (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) (hcard : ↑(d + 1) < ENat.card k) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : genus k F = (d - 1) * (d - 2) / 2

The genus of a smooth projective plane curve, over a constant field with more than d + 1 elements: let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d with every point of G = 0 over an algebraically closed extension K of k nonsingular, and let F / k be generated by a transcendental x and an element y with G(x, y, 1) = 0, where k is the exact constant field of F. If k has more than d + 1 elements, then F has genus (d - 1)(d - 2) / 2.

theorem TauCeti.isIntegrallyClosedIn_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : IsIntegrallyClosedIn k F

The constant field of a smooth projective plane curve: let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, with every point of G = 0 over an algebraically closed extension K of k nonsingular, and let F / k be generated by a transcendental x and an element y with G(x, y, 1) = 0. Then k is the exact constant field of F: nonsingularity makes G(X₀, X₁, 1) irreducible over K (TauCeti.isIntegrallyClosedIn_of_irreducible_map for the affine equation).

theorem TauCeti.genus_eq_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : F} (hx : Transcendental k x) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : genus k F = (d - 1) * (d - 2) / 2

The genus of a smooth projective plane curve (Fulton, Algebraic Curves, Section 8.3): let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, with every point of G = 0 over an algebraically closed extension K of k nonsingular. Let F / k be generated by a transcendental x and an element y with G(x, y, 1) = 0. Then F has genus (d - 1)(d - 2) / 2.

Nonsingularity makes G(X₀, X₁, 1) irreducible over K, so k is the exact constant field of F (TauCeti.isIntegrallyClosedIn_of_irreducible_map).

theorem TauCeti.genus_eq_of_isHomogeneous_of_aeval_insertNth_eq_zero {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) (i : Fin 3) {x y : F} (hxy : Transcendental k x ∨ Transcendental k y) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval (i.insertNth 1 ![x, y])) G = 0) : genus k F = (d - 1) * (d - 2) / 2

The genus of a smooth projective plane curve, in any affine chart: as TauCeti.genus_eq_of_isHomogeneous, for a point (x, y) of G = 0 in the chart Xᵢ = 1, whose homogeneous coordinates are x and y in the remaining positions in increasing order and 1 at position i, and with either x or y transcendental.

theorem TauCeti.isIntegrallyClosedIn_of_isHomogeneous_of_aeval_insertNth_eq_zero {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) (i : Fin 3) {x y : F} (hxy : Transcendental k x ∨ Transcendental k y) (hgen : k⟮x, y⟯ = ⊤) (h : (MvPolynomial.aeval (i.insertNth 1 ![x, y])) G = 0) : IsIntegrallyClosedIn k F

The constant field of a smooth projective plane curve, in any affine chart: as TauCeti.isIntegrallyClosedIn_of_isHomogeneous, for a point (x, y) of G = 0 in the chart Xᵢ = 1, whose homogeneous coordinates are x and y in the remaining positions in increasing order and 1 at position i, and with either x or y transcendental.

The canonical class

theorem TauCeti.degree_sup_poles_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hF : IsFunctionField k F) (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : Fˣ} (hx : Transcendental k ↑x) (hgen : k⟮↑x, ↑y⟯ = ⊤) (h : (MvPolynomial.aeval ![↑x, ↑y, 1]) G = 0) : Divisor.degree (Divisor.poles hF x ⊔ Divisor.poles hF y) = ↑d

The line at infinity meets a smooth projective plane curve of degree d in d points, counted with multiplicities and residue degrees: let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, with every point of G = 0 over an algebraically closed extension K of k nonsingular, and let F / k be generated by nonzero x and y with G(x, y, 1) = 0 and x transcendental. Then the divisor (x)_∞ ⊔ (y)_∞ cut out on the curve by the line at infinity X₂ = 0 has degree d.

theorem TauCeti.linearIndepOn_pow_mul_pow_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : F} (hx : Transcendental k x) (h : (MvPolynomial.aeval ![x, y, 1]) G = 0) : LinearIndepOn k (fun (p : ℕ × ℕ) => x ^ p.1 * y ^ p.2) {p : ℕ × ℕ | p.1 + p.2 < d}

The monomials of degree less than d on a smooth projective plane curve are linearly independent: under the hypotheses of TauCeti.genus_eq_of_isHomogeneous, except that x and y need not generate F, the products x ^ i y ^ j with i + j < d are linearly independent over k.

theorem TauCeti.divisorClass_sub_three_zsmul_sup_poles_eq_canonicalClass_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : Fˣ} (hx : Transcendental k ↑x) (hgen : k⟮↑x, ↑y⟯ = ⊤) (h : (MvPolynomial.aeval ![↑x, ↑y, 1]) G = 0) : (Place.orderSystem hF).divisorClass ((↑d - 3) • (Divisor.poles hF x ⊔ Divisor.poles hF y)) = canonicalClass hF hex

The canonical class of a smooth projective plane curve of degree d is (d - 3) H: let G ∈ k[X₀, X₁, X₂] be homogeneous of degree d, with every point of G = 0 over an algebraically closed extension K of k nonsingular, and let F / k be generated by nonzero x and y with G(x, y, 1) = 0 and x transcendental. Then (d - 3) H represents the canonical class, where H = (x)_∞ ⊔ (y)_∞ is the divisor cut out by the line at infinity. For d ≥ 3 this says that the effective canonical divisors are cut out by the curves of degree d - 3; for d = 1, 2 the coefficient d - 3 is negative and the statement is the signed formula. (The exactness of the constant field k, which the canonical class needs, follows from nonsingularity by TauCeti.isIntegrallyClosedIn_of_isHomogeneous.)

theorem TauCeti.riemannRochSpace_sub_three_zsmul_sup_poles_eq_span_of_isHomogeneous {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {K : Type u_3} [Field K] [IsAlgClosed K] [Algebra k K] {G : MvPolynomial (Fin 3) k} {d : ℕ} (hF : IsFunctionField k F) (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin 3 → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin 3), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) {x y : Fˣ} (hx : Transcendental k ↑x) (hgen : k⟮↑x, ↑y⟯ = ⊤) (h : (MvPolynomial.aeval ![↑x, ↑y, 1]) G = 0) : riemannRochSpace ((↑d - 3) • (Divisor.poles hF x ⊔ Divisor.poles hF y)) = Submodule.span k ((fun (p : ℕ × ℕ) => ↑x ^ p.1 * ↑y ^ p.2) '' {p : ℕ × ℕ | p.1 + p.2 + 3 ≤ d})

The Riemann–Roch space of the canonical divisor of a smooth projective plane curve: under the hypotheses of TauCeti.divisorClass_sub_three_zsmul_sup_poles_eq_canonicalClass_of_isHomogeneous, L((d - 3) ((x)_∞ ⊔ (y)_∞)) is spanned by the monomials x ^ i y ^ j with i + j ≤ d - 3, which are linearly independent (TauCeti.linearIndepOn_pow_mul_pow_of_isHomogeneous): it is the space of polynomials in x and y of degree at most d - 3.