Documentation

TauCeti.FieldTheory.FunctionField.RiemannRoch.Pencil

Multiplication by the pencil of a function #

For a nonzero function z, write Z and D for its zero and pole divisors. The sections 1, z of L(D) have no common zero; for nonconstant z they form a pencil. If deg (A - Z) > 2g - 2, then every element of L(A + D) is a + z b with a, b ∈ L(A). The results also allow constant z.

In particular, for D = (z)∞ and sufficiently large n, L((n + 1)D) = L(nD) + z L(nD). Iteration expresses all higher sections using powers of z and a single finite-dimensional space of sections. This is the multiplication input for finite generation of the section ring TauCeti.Divisor.sectionRing D over the subalgebra generated by its two degree-one sections 1, z; for z transcendental over k, D has positive degree and this subalgebra is a polynomial algebra in two variables. In product form, L((n + 1)D) ⊆ L(D) · L(nD) in the same range (TauCeti.riemannRochSpace_succ_nsmul_poles_le_mul).

Iterating the product form, once 2g - 1 ≤ (N - 1) deg D every section of (N + j) D is a sum of products of j sections of D with one of N D (TauCeti.riemannRochSpace_add_nsmul_poles_le_pow_mul). Since L(D)ᵉ ⊆ L(eD), it follows that the section ring of eD is generated in degree one as soon as 2g - 1 ≤ (e - 1) deg D (TauCeti.riemannRochSpace_nsmul_nsmul_poles_le_pow), with no finite-generation argument for the section ring of D. For z transcendental over k, deg D ≥ 1, so this applies to the pole divisor (zᵉ)∞ = e D of every power zᵉ with e ≥ 1 and e ≥ 2g (TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow). In genus zero it applies to D itself, so the section ring of every pole divisor is generated in degree one (TauCeti.riemannRochSpace_nsmul_poles_le_pow_of_genus_eq_zero). Generation in degree one is what embeds a curve in projective space by the complete linear system of the divisor.

These statements use Riemann–Roch, so they need k to be the exact constant field of F. Over an arbitrary k, the multiples of a pole divisor have the same Riemann–Roch spaces over k and over the full constant field K = algebraicClosure k F (TauCeti.restrictScalars_riemannRochSpace_nsmul_poles), and K is exact. So generation in every positive degree persists over k, for e ≥ 2 g(F / K) (TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow_of_ne_zero). Only degree zero is lost, where L(0) = K is larger than the constants k unless k is exact; projective embeddings do not see degree zero.

The argument is the base-point-free pencil calculation: the intersection of L(A) and z L(A) is L(A - Z), and Riemann–Roch computes the dimension of their sum. Multiplication by z is the existing equivalence TauCeti.riemannRochSpaceEquivSubPrincipal.

References #

theorem TauCeti.riemannRochSpace_add_poles_eq_sup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) (A : Divisor k F) (hA : 2 * ↑(genus k F) - 1 ≤ Divisor.degree (A - Divisor.zeros hF z)) :

The pencil 1, z generates L(A + (z)∞) from L(A) in high degree. The second summand is z L(A), expressed as a Riemann–Roch space via the principal divisor.

theorem TauCeti.mem_riemannRochSpace_add_poles_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) (A : Divisor k F) (hA : 2 * ↑(genus k F) - 1 ≤ Divisor.degree (A - Divisor.zeros hF z)) (f : F) :
f ∈ riemannRochSpace (A + Divisor.poles hF z) ↔ ∃ a ∈ riemannRochSpace A, ∃ b ∈ riemannRochSpace A, f = a + ↑z * b

Every section of A + (z)∞ decomposes as a + z b with both terms drawn from L(A), provided A - (z)₀ has degree above the canonical degree.

theorem TauCeti.mem_riemannRochSpace_succ_nsmul_poles_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) (n : ℕ) (hn : 2 * ↑(genus k F) - 1 ≤ (↑n - 1) * Divisor.degree (Divisor.poles hF z)) (f : F) :
f ∈ riemannRochSpace ((n + 1) • Divisor.poles hF z) ↔ ∃ a ∈ riemannRochSpace (n • Divisor.poles hF z), ∃ b ∈ riemannRochSpace (n • Divisor.poles hF z), f = a + ↑z * b

Multiplication by 1, z generates the next multiple of the pole divisor. The bound is on the preceding multiple, so all three Riemann–Roch dimensions are in high degree.

theorem TauCeti.riemannRochSpace_succ_nsmul_poles_le_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) (n : ℕ) (hn : 2 * ↑(genus k F) - 1 ≤ (↑n - 1) * Divisor.degree (Divisor.poles hF z)) :

In the same range, every section of (n + 1) D, for D = (z)∞, is a sum of products of a section of D with a section of nD, since the pencil 1, z lies in L(D). This is the multiplication condition under which the section ring of D is generated in degree one.

theorem TauCeti.riemannRochSpace_add_nsmul_poles_le_pow_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) {N : ℕ} (hN : 2 * ↑(genus k F) - 1 ≤ (↑N - 1) * Divisor.degree (Divisor.poles hF z)) (j : ℕ) :

Iterating the pencil: once the bound holds at N, every section of (N + j) D, for D = (z)∞, is a sum of products of j sections of D with a section of N D.

theorem TauCeti.riemannRochSpace_nsmul_nsmul_poles_le_pow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) {e : ℕ} (he : 2 * ↑(genus k F) - 1 ≤ (↑e - 1) * Divisor.degree (Divisor.poles hF z)) (n : ℕ) :

The section ring of a multiple of a pole divisor is generated in degree one once the multiple is in the range of the pencil: if 2g - 1 ≤ (e - 1) deg D for D = (z)∞, then every section of n (e D) is a sum of products of n sections of e D, over an exact constant field.

theorem TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {z : Fˣ} (hz : Transcendental k ↑z) {e : ℕ} (he₀ : 0 < e) (he : 2 * genus k F ≤ e) (n : ℕ) :

High powers of a transcendental function have pole divisors whose section ring is generated in degree one: over an exact constant field, if z is transcendental over k, e ≥ 1 and e ≥ 2g, then every section of n (zᵉ)∞ is a sum of products of n sections of (zᵉ)∞.

theorem TauCeti.riemannRochSpace_nsmul_poles_pow_le_pow_of_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {z : Fˣ} (hz : Transcendental k ↑z) {e : ℕ} (he₀ : 0 < e) (he : 2 * genus (↥(algebraicClosure k F)) F ≤ e) {n : ℕ} (hn : n ≠ 0) :

High powers of a transcendental function have pole divisors whose section ring is generated in positive degrees, over any constant field: if z is transcendental over k, e ≥ 1 and e ≥ 2g, where g is the genus of F over its full constant field algebraicClosure k F, then for every n ≠ 0, every section of n (zᵉ)∞ is a sum of products of n sections of (zᵉ)∞. Degree zero is excluded: L(0) is algebraicClosure k F, which is larger than the constants k unless k is the exact constant field.

In genus zero, the section ring of a pole divisor is generated in degree one: over an exact constant field, every section of n D, for D = (z)∞, is a sum of products of n sections of D.

theorem TauCeti.riemannRochSpace_add_nsmul_poles_eq_span {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) (N : ℕ) (hN : 2 * ↑(genus k F) - 1 ≤ (↑N - 1) * Divisor.degree (Divisor.poles hF z)) (m : ℕ) :
riemannRochSpace ((N + m) • Divisor.poles hF z) = Submodule.span k {f : F | ∃ i ≤ m, ∃ a ∈ riemannRochSpace (N • Divisor.poles hF z), f = ↑z ^ i * a}

All higher sections are generated by one space L(ND) and bounded powers of z, where D = (z)∞. Thus a basis of L(ND) supplies finitely many generators for the high-degree part of the section ring as a module over the pencil 1, z.