The section ring of a divisor

Let F / k be an algebraic function field and D a divisor of F. Since L(mD) · L(nD) ⊆ L((m + n)D), the Riemann–Roch spaces L(nD), n ∈ ℕ, form a graded family of k-subspaces of F, and their direct sum ⨁ₙ L(nD) is a graded k-algebra, the section ring of D. It is realized as the subalgebra TauCeti.Divisor.sectionRing D of F[X] of polynomials ∑ fₙ Xⁿ with fₙ ∈ L(nD), graded by the power of X.

Section rings of divisors are the graded rings from which projective models of a curve are built as Proj. If a section ring is finitely generated, then sufficiently divisible Veronese subrings are generated in degree one: for some e > 0, and every positive multiple e' of e, L(m e' D) = L(e' D) ^ m for m > 0. This file also computes the rings of the standard affine charts D₊(f Xⁿ) of Proj of the section ring, and which of these charts cover it. If f Xⁿ is homogeneous of degree n with f ∈ L(nD) nonzero, the degree-zero fractions g Xⁿʳ / (f Xⁿ)ʳ, with g ∈ L(nrD), are the functions g / fʳ, and these are exactly the functions regular at every place P at which f attains the bound ord_P f ≥ -n D(P) defining L(nD), that is, every place outside the support of the effective divisor div f + nD. So the homogeneous localization at f Xⁿ is a holomorphy ring (TauCeti.Divisor.sectionRingAwayEquiv). Sections sᵢ ∈ L(D) without a common base point, meaning that at every place P one of them has order exactly -D(P), give elements sᵢ X of degree one whose standard opens cover Proj (TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne).

For the pole divisor D = (x)_∞ of a nonzero x and the sections 1, x ∈ L(D), the two holomorphy rings are the rings 𝒪_x and 𝒪_{x⁻¹} of functions regular wherever x, respectively x⁻¹, is regular (TauCeti.Divisor.coeff_poles_eq_zero_iff and TauCeti.Divisor.valuation_eq_exp_coeff_poles_iff), and 1, x have no common base point (TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne_poles). These are the two affine charts from which TauCeti.AlgebraicGeometry.twoChartModel is glued.

The section ring is generated by its elements s X of degree one exactly when L(nD) ⊆ L(D)ⁿ for every n (TauCeti.Divisor.adjoin_sectionRingGrade_one_eq_top_iff). In degree zero this asks that L(0) be k, which holds exactly for an exact constant field, but Proj only sees positive degrees: if L(nD) ⊆ L(D)ⁿ for every n ≠ 0, then Proj of the section ring is a closed subscheme of the projective space of L(D), by AlgebraicGeometry.Proj.isClosedImmersion_map_gradedLift and TauCeti.Divisor.sectionRingGrade_subset_adjoin_range_sectionRingGradeOneEquiv_iff.

Main definitions

• TauCeti.Divisor.sectionRing D: the section ring ⨁ₙ L(nD) of D, inside F[X].
• TauCeti.Divisor.sectionRingGrade D: its grading, n ↦ L(nD) Xⁿ.
• TauCeti.Divisor.monomialDegreeOne hs: the element s X of degree one, for s ∈ L(D).
• TauCeti.Divisor.sectionRingGradeOneEquiv D: the isomorphism s ↦ s X from L(D) onto the degree-one piece.
• TauCeti.Divisor.sectionRingAwayEquiv hF hf hf0: for a nonzero homogeneous element f Xⁿ, the isomorphism from the homogeneous localization at f Xⁿ onto the holomorphy ring of the places at which f has valuation exp (n D(P)).
• TauCeti.Divisor.sectionRingAwayOneEquiv hF z and TauCeti.Divisor.sectionRingAwayGeneratorEquiv hF z: the homogeneous localizations of the section ring of (z)_∞ at X and at z X are the holomorphy rings 𝒪_z and 𝒪_{z⁻¹}.

Main results

• TauCeti.Divisor.mem_holomorphyRing_iff_exists_mul_pow_mem_riemannRochSpace: for f ∈ L(nD), a function z is regular at every place P where ord_P f = -n D(P) exactly when z fʳ ∈ L(nrD) for some r.
• TauCeti.Divisor.exists_riemannRochSpace_mul_eq_pow: if the section ring of D is finitely generated, then sufficiently divisible section rings are generated in degree one.
• TauCeti.Divisor.sectionRingAwayEquiv_mk: the isomorphism sends g Xⁿʳ / (f Xⁿ)ʳ to g / fʳ.
• TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne: sections of L(D) without a common base point generate the irrelevant ideal up to radical.
• TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne_poles: for D = (x)_∞, the elements X and x X generate the irrelevant ideal up to radical.
• TauCeti.Divisor.adjoin_sectionRingGrade_one_eq_top_iff: the section ring is generated in degree one exactly when L(nD) ⊆ L(D)ⁿ for every n.
• TauCeti.Divisor.adjoin_range_sectionRingGradeOneEquiv_eq_top_iff: the same condition, stated as generation by the image of L(D).
• TauCeti.Divisor.sectionRingGrade_subset_adjoin_range_sectionRingGradeOneEquiv_iff: the elements of degree n are generated by the image of L(D) exactly when L(nD) ⊆ L(D)ⁿ; for every n ≠ 0, this is the hypothesis of AlgebraicGeometry.Proj.isClosedImmersion_map_gradedLift.
• TauCeti.Divisor.adjoin_sectionRingGrade_one_eq_top: over an exact constant field, it is generated in degree one as soon as L((n + 1)D) ⊆ L(D) L(nD) for every n ≥ 1.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.2 (the affine charts of Proj) and Section IV.3 (embedding a curve by the sections of a divisor).
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2 (holomorphy rings) and Theorem 1.1.19.

The section ring and its grading

instance TauCeti.Divisor.gradedMonoid_riemannRochSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : SetLike.GradedMonoid fun (n : ℕ) => riemannRochSpace (n • D)

The Riemann–Roch spaces L(nD) form a graded family: 1 ∈ L(0) and L(mD) · L(nD) ⊆ L((m + n)D).

@[reducible, inline]

noncomputable abbrev TauCeti.Divisor.sectionRing {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : Subalgebra k (Polynomial F)

The section ring ⨁ₙ L(nD) of a divisor D: the k-subalgebra of F[X] of polynomials ∑ fₙ Xⁿ with fₙ ∈ L(nD) for every n.

It is an abbreviation for TauCeti.coeffSubalgebra of the family n ↦ L(nD), so that the grading and its API apply to it directly.

@[reducible, inline]

noncomputable abbrev TauCeti.Divisor.sectionRingGrade {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : ℕ → Submodule k ↥D.sectionRing

The grading of the section ring of D: its degree n piece consists of the monomials f Xⁿ with f ∈ L(nD).

noncomputable def TauCeti.Divisor.monomialDegreeOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {s : F} (hs : s ∈ riemannRochSpace D) : ↥D.sectionRing

The element s X of degree one of the section ring of D, for s ∈ L(D).

@[simp]

theorem TauCeti.Divisor.coe_monomialDegreeOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {s : F} (hs : s ∈ riemannRochSpace D) : ↑(monomialDegreeOne hs) = (Polynomial.monomial 1) s

theorem TauCeti.Divisor.monomialDegreeOne_mem_sectionRingGrade {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {s : F} (hs : s ∈ riemannRochSpace D) : monomialDegreeOne hs ∈ D.sectionRingGrade 1

noncomputable def TauCeti.Divisor.sectionRingGradeOneEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : ↥(riemannRochSpace D) ≃ₗ[k] ↥(D.sectionRingGrade 1)

The k-linear isomorphism s ↦ s X from L(D) onto the degree-one piece of the section ring of D.

@[simp]

theorem TauCeti.Divisor.coe_sectionRingGradeOneEquiv_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (s : ↥(riemannRochSpace D)) : ↑(D.sectionRingGradeOneEquiv s) = monomialDegreeOne ⋯

@[simp]

theorem TauCeti.Divisor.coe_sectionRingGradeOneEquiv_symm_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : ↥(D.sectionRingGrade 1)) : ↑(D.sectionRingGradeOneEquiv.symm f) = (↑↑f).coeff 1

Generation in degree one

theorem TauCeti.Divisor.adjoin_sectionRingGrade_one_eq_top_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} : Algebra.adjoin k ↑(D.sectionRingGrade 1) = ⊤ ↔ ∀ (n : ℕ), riemannRochSpace (n • D) ≤ riemannRochSpace D ^ n

The section ring of D is generated in degree one exactly when L(nD) ⊆ L(D)ⁿ for every n, that is, when every function in L(nD) is a sum of products of n functions in L(D). For n = 0 this asks that L(0) be the constants k, which holds exactly when k is the exact constant field of F (TauCeti.riemannRochSpace_zero).

theorem TauCeti.Divisor.adjoin_range_sectionRingGradeOneEquiv_eq_top_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} : Algebra.adjoin k (Set.range fun (s : ↥(riemannRochSpace D)) => ↑(↑D.sectionRingGradeOneEquiv s)) = ⊤ ↔ ∀ (n : ℕ), riemannRochSpace (n • D) ≤ riemannRochSpace D ^ n

The elements s X, s ∈ L(D), generate the section ring of D exactly when L(nD) ⊆ L(D)ⁿ for every n. In this form the condition is the generation hypothesis of SymmetricAlgebra.gradedLift_surjective for the linear map (sectionRingGradeOneEquiv D).toLinearMap: Sym_k L(D) then maps onto the section ring.

theorem TauCeti.Divisor.sectionRingGrade_subset_adjoin_range_sectionRingGradeOneEquiv_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {n : ℕ} : ↑(D.sectionRingGrade n) ⊆ ↑(Algebra.adjoin k (Set.range fun (s : ↥(riemannRochSpace D)) => ↑(↑D.sectionRingGradeOneEquiv s))) ↔ riemannRochSpace (n • D) ≤ riemannRochSpace D ^ n

Generation in a single degree. The elements f Xⁿ, f ∈ L(nD), of degree n of the section ring of D lie in the subalgebra generated by the elements s X, s ∈ L(D), exactly when L(nD) ⊆ L(D)ⁿ. For every n ≠ 0, this is the generation hypothesis of AlgebraicGeometry.Proj.isClosedImmersion_map_gradedLift for the linear map (sectionRingGradeOneEquiv D).toLinearMap: Proj of the section ring is then a closed subscheme of Proj (Sym_k L(D)). Unlike generation of the whole section ring, it does not ask that L(0) be k.

theorem TauCeti.Divisor.adjoin_sectionRingGrade_one_eq_top {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {D : Divisor k F} (hD : ∀ (n : ℕ), n ≠ 0 → riemannRochSpace ((n + 1) • D) ≤ riemannRochSpace D * riemannRochSpace (n • D)) : Algebra.adjoin k ↑(D.sectionRingGrade 1) = ⊤

A criterion for generation in degree one. If k is the exact constant field of F and the products L(D) · L(nD) span L((n + 1)D) for every n ≥ 1, then the section ring of D is generated by its elements s X of degree one, s ∈ L(D).

Functions regular where a section attains its bound

theorem TauCeti.Divisor.mem_holomorphyRing_iff_exists_mul_pow_mem_riemannRochSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {n : ℕ} {f : F} (hf : f ∈ riemannRochSpace (n • D)) {z : F} : z ∈ holomorphyRing {P : Place k F | P.valuation f = WithZero.exp (↑n * AlgebraicGeometry.WeilDivisor.coeff D P)} ↔ ∃ (r : ℕ), z * f ^ r ∈ riemannRochSpace ((n * r) • D)

Functions regular where a section attains its bound. Let f ∈ L(nD). A function z is regular at every place P at which f has valuation exp (n D(P)), that is, ord_P f = -n D(P), so that f attains the bound defining L(nD), exactly when z fʳ ∈ L(nrD) for some r: the other places are zeros of the effective divisor div f + nD, where a high power of f absorbs the poles of z.

At f = 0 the set of places is empty and both sides hold for every z.

Veronese section rings

noncomputable def TauCeti.Divisor.evalOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : ↥D.sectionRing →ₐ[k] F

Evaluation at X = 1, ∑ fₙ Xⁿ ↦ ∑ fₙ, on the section ring. It sends a homogeneous element f Xⁿ to f.

theorem TauCeti.Divisor.evalOne_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : ↥D.sectionRing) : D.evalOne f = Polynomial.eval 1 ↑f

Evaluation at X = 1 on the section ring is polynomial evaluation at 1.

theorem TauCeti.Divisor.evalOne_of_mem {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {n : ℕ} {f : ↥D.sectionRing} (hf : f ∈ D.sectionRingGrade n) : D.evalOne f = (↑f).coeff n

On a homogeneous element of degree n, evaluation at X = 1 is the n-th coefficient.

theorem TauCeti.Divisor.exists_riemannRochSpace_mul_eq_pow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) [Algebra.FiniteType k ↥D.sectionRing] : ∃ (e : ℕ), 0 < e ∧ ∀ ⦃e' : ℕ⦄, e ∣ e' → ∀ ⦃m : ℕ⦄, m ≠ 0 → riemannRochSpace ((m * e') • D) = riemannRochSpace (e' • D) ^ m

Sufficiently divisible section rings are generated in degree one. If the section ring of D is finitely generated over k, then there is an e > 0 such that for every multiple e' of e and every m > 0, every section in L(m e' D) is a sum of products of m sections in L(e' D).

The homogeneous localizations of the section ring

noncomputable def TauCeti.Divisor.sectionRingAwayEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {n : ℕ} {f : ↥D.sectionRing} (hf : f ∈ D.sectionRingGrade n) (hf0 : f ≠ 0) : HomogeneousLocalization.Away D.sectionRingGrade f ≃ₐ[k] ↥(holomorphyRing {P : Place k F | P.valuation ((↑f).coeff n) = WithZero.exp (↑n * AlgebraicGeometry.WeilDivisor.coeff D P)})

The homogeneous localization of the section ring at a nonzero homogeneous element. Let f Xⁿ be a nonzero homogeneous element of degree n of the section ring of D, so f ∈ L(nD). Its homogeneous localization, the ring of fractions g Xⁿʳ / (f Xⁿ)ʳ with g ∈ L(nrD), is isomorphic to the holomorphy ring of the places at which f has valuation exp (n D(P)), that is, ord_P f = -n D(P); the fraction corresponds to g / fʳ (TauCeti.Divisor.sectionRingAwayEquiv_mk).

Geometrically, the standard open D₊(f Xⁿ) of Proj of the section ring is the spectrum of the ring of functions regular outside the support of div f + nD.

@[simp]

theorem TauCeti.Divisor.sectionRingAwayEquiv_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {n : ℕ} {f : ↥D.sectionRing} (hf : f ∈ D.sectionRingGrade n) (hf0 : f ≠ 0) (r : ℕ) (g : ↥D.sectionRing) (hg : g ∈ D.sectionRingGrade (r • n)) : ↑((sectionRingAwayEquiv hF hf hf0) (HomogeneousLocalization.Away.mk D.sectionRingGrade hf r g hg)) = (↑g).coeff (r • n) * ((↑f).coeff n ^ r)⁻¹

The isomorphism TauCeti.Divisor.sectionRingAwayEquiv sends the fraction g Xⁿʳ / (f Xⁿ)ʳ to g / fʳ.

Sections without a common base point cover Proj

theorem TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {ι : Type u_3} {s : ι → F} (hs : ∀ (i : ι), s i ∈ riemannRochSpace D) (hbase : ∀ (P : Place k F), ∃ (i : ι), P.valuation (s i) = WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)) : (HomogeneousIdeal.irrelevant D.sectionRingGrade).toIdeal ≤ (Ideal.span (Set.range fun (i : ι) => monomialDegreeOne ⋯)).radical

Sections without a common base point cover Proj of the section ring. If the sections sᵢ ∈ L(D) have no common base point, that is, at every place P some sᵢ has valuation exp (D(P)) (equivalently, ord_P sᵢ = -D(P)), then the elements sᵢ X of degree one generate the irrelevant ideal of the section ring of D up to radical. Equivalently, the standard opens D₊(sᵢ X) cover Proj of the section ring.

The pole divisor of a function

theorem TauCeti.Divisor.irrelevant_le_radical_span_monomialDegreeOne_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : (HomogeneousIdeal.irrelevant (poles hF z).sectionRingGrade).toIdeal ≤ (Ideal.span {monomialDegreeOne ⋯, monomialDegreeOne ⋯}).radical

The sections 1 and z of the pole divisor of z cover Proj of its section ring: the elements X and z X of degree one generate the irrelevant ideal up to radical.

@[reducible, inline]

noncomputable abbrev TauCeti.Divisor.polesSectionOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : ↥(poles hF z).sectionRing

The degree-one section X in the section ring of the pole divisor of z.

@[reducible, inline]

noncomputable abbrev TauCeti.Divisor.polesSectionGenerator {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : ↥(poles hF z).sectionRing

The degree-one section z X in the section ring of the pole divisor of z.

noncomputable def TauCeti.Divisor.sectionRingAwayOneEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : HomogeneousLocalization.Away (poles hF z).sectionRingGrade (polesSectionOne hF z) ≃ₐ[k] ↥(holomorphyRing {P : Place k F | ↑z ∈ P.integers})

Localizing the section ring of (z)_∞ at X gives the holomorphy ring of the places at which z is regular.

@[simp]

theorem TauCeti.Divisor.sectionRingAwayOneEquiv_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (r : ℕ) (g : ↥(poles hF z).sectionRing) (hg : g ∈ (poles hF z).sectionRingGrade r) : ↑((sectionRingAwayOneEquiv hF z) (HomogeneousLocalization.Away.mk (poles hF z).sectionRingGrade ⋯ r g ⋯)) = (↑g).coeff r

Under TauCeti.Divisor.sectionRingAwayOneEquiv, the fraction g Xʳ / Xʳ is sent to the degree-r coefficient of g.

noncomputable def TauCeti.Divisor.sectionRingAwayGeneratorEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : HomogeneousLocalization.Away (poles hF z).sectionRingGrade (polesSectionGenerator hF z) ≃ₐ[k] ↥(holomorphyRing {P : Place k F | (↑z)⁻¹ ∈ P.integers})

Localizing the section ring of (z)_∞ at z X gives the holomorphy ring of the places at which z⁻¹ is regular.

@[simp]

theorem TauCeti.Divisor.sectionRingAwayGeneratorEquiv_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (r : ℕ) (g : ↥(poles hF z).sectionRing) (hg : g ∈ (poles hF z).sectionRingGrade r) : ↑((sectionRingAwayGeneratorEquiv hF z) (HomogeneousLocalization.Away.mk (poles hF z).sectionRingGrade ⋯ r g ⋯)) = (↑g).coeff r * (↑z ^ r)⁻¹

Under TauCeti.Divisor.sectionRingAwayGeneratorEquiv, the fraction g Xʳ / (z X)ʳ is sent to g / zʳ.