Riemann–Roch spaces

The Riemann–Roch space of a divisor D of an algebraic function field F / k is the k-subspace

L(D) = {f : F | div f + D ≥ 0}

of functions whose poles are bounded by D, and ℓ(D) = dim_k L(D) is its dimension. This file constructs L(D), proves the two computations that pin it down at the bottom of the divisor order, and proves that it is always finite-dimensional with the sharp bound ℓ(D) ≤ deg D⁺ + 1 over an exact constant field. It is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definition 1.4.4 through Definition 1.4.10.

Main definitions

• TauCeti.riemannRochSpace: the Riemann–Roch space L(D) : Submodule k F (Definition 1.4.4). Its membership condition is the multiplicative v_P f ≤ exp (D P), which is junk-free at f = 0 — no separate ∪ {0} clause is needed, unlike in the additive ord_P form.
• TauCeti.Divisor.dim: the dimension ℓ(D) = dim_k L(D) (Definition 1.4.10).

Main results

• TauCeti.one_mem_riemannRochSpace_iff: 1 ∈ L(D) exactly when D is effective.
• TauCeti.mul_mem_riemannRochSpace_add: multiplication maps L(A) × L(B) into L(A + B).
• TauCeti.riemannRochSpace_zero: L(0) is the field of constants algebraicClosure k F — over an exact constant field, L(0) = k (TauCeti.riemannRochSpace_zero_of_isIntegrallyClosedIn, Lemma 1.4.7(a)).
• TauCeti.riemannRochSpace_eq_bot_of_lt_zero: L(D) = 0 for D < 0 (Lemma 1.4.7(b)).
• TauCeti.riemannRochSpace_sub_ofFinset_eq: if removing any single place of a finite set T leaves L(D) unchanged, so does removing all of T at once.
• TauCeti.finrank_riemannRochSpace_add_ofPoint_le: adding one place to a divisor raises ℓ by at most the degree of that place (Lemma 1.4.8, the one-place-at-a-time estimate).
• TauCeti.finrank_quotient_riemannRochSpace_le_degree_sub: for D ≤ E the quotient L(E)/L(D) has dimension at most deg E - deg D, equivalently TauCeti.Divisor.dim_le_dim_add_degree_sub: ℓ(E) ≤ ℓ(D) + (deg E - deg D) (Lemma 1.4.8).
• TauCeti.rank_quotient_riemannRochSpace_add_dim: the rank of L(E)/L(D) is exactly ℓ(E) - ℓ(D), in the subtraction-free form rank (L(E)/L(D)) + ℓ(D) = ℓ(E).
• TauCeti.finiteDimensional_riemannRochSpace and TauCeti.Divisor.dim_le_degree_posPart_add_one: L(D) is finite-dimensional, with ℓ(D) ≤ deg D⁺ + [algebraicClosure k F : k] and hence ℓ(D) ≤ deg D⁺ + 1 over an exact constant field (Proposition 1.4.9).

Finite-dimensionality and the estimates leading to it are proved with no hypothesis on the constant field; only the sharp + 1 needs IsIntegrallyClosedIn k F. For a non-exact constant field the bound genuinely degrades: over ℝ ⊂ ℂ(x) already ℓ(0) = 2.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4.

noncomputable def TauCeti.riemannRochSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : Submodule k F

The Riemann–Roch space L(D) of a divisor D of F / k (Stichtenoth, Definition 1.4.4): the k-subspace of functions whose poles are bounded by D, that is div f + D ≥ 0.

The membership condition is stated multiplicatively as v_P f ≤ exp (D P). This is junk-free at f = 0, where the valuation is 0 and the condition holds at every place, so no separate ∪ {0} clause is needed; the additive form is TauCeti.mem_riemannRochSpace_iff_neg_le_ord.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.Divisor.dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : ℕ

ℓ(D) = dim_k L(D) (Stichtenoth, Definition 1.4.10). Its finiteness, which guards the junk value of Module.finrank, is TauCeti.finiteDimensional_riemannRochSpace.

Equations

• D.dim = Module.finrank k ↥(TauCeti.riemannRochSpace D)

theorem TauCeti.Divisor.dim_def {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : D.dim = Module.finrank k ↥(riemannRochSpace D)

ℓ(D) unfolded to the dimension of L(D).

@[simp]

theorem TauCeti.mem_riemannRochSpace_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : F} : f ∈ riemannRochSpace D ↔ ∀ (P : Place k F), P.valuation f ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)

Membership in L(D), unfolded: the poles of f are bounded by D at every place.

theorem TauCeti.mem_riemannRochSpace_iff_neg_le_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : F} (hf : f ≠ 0) : f ∈ riemannRochSpace D ↔ ∀ (P : Place k F), -AlgebraicGeometry.WeilDivisor.coeff D P ≤ P.ord f

The additive form of membership in L(D): away from the junk value ord_P 0 = 0, the functions of L(D) are those with ord_P f ≥ -D P at every place.

theorem TauCeti.mem_riemannRochSpace_zsmul_ofPoint_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {n : ℤ} {f : F} (hf : f ≠ 0) : f ∈ riemannRochSpace (n • AlgebraicGeometry.WeilDivisor.ofPoint P) ↔ -n ≤ P.ord f ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord f

Membership in L(nP) for a single place P: a nonzero function lies in L(nP) exactly when its order at P is at least -n and it is regular at every other place.

theorem TauCeti.riemannRochSpace_mono {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) : riemannRochSpace D ≤ riemannRochSpace E

Enlarging a divisor enlarges its Riemann–Roch space (Stichtenoth, Lemma 1.4.8, first part).

theorem TauCeti.riemannRochSpace_monotone {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] : Monotone riemannRochSpace

The bundled form of TauCeti.riemannRochSpace_mono.

theorem TauCeti.riemannRochSpace_sub_ofFinset_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {T : Finset (Place k F)} (hT : ∀ P ∈ T, riemannRochSpace (D - AlgebraicGeometry.WeilDivisor.ofPoint P) = riemannRochSpace D) : riemannRochSpace (D - AlgebraicGeometry.WeilDivisor.ofFinset T) = riemannRochSpace D

If removing any single place of a finite set T leaves L(D) unchanged, then so does removing all of T at once: L(D - ∑_{P ∈ T} P) = L(D).

theorem TauCeti.one_mem_riemannRochSpace_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} : 1 ∈ riemannRochSpace D ↔ 0 ≤ D

The constant function 1 belongs to L(D) exactly when D is effective.

Not a simp lemma: TauCeti.mem_riemannRochSpace_iff already rewrites the left-hand side place by place, so this statement is not in simp-normal form.

theorem TauCeti.mul_mem_riemannRochSpace_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {A B : Divisor k F} {f g : F} (hf : f ∈ riemannRochSpace A) (hg : g ∈ riemannRochSpace B) : f * g ∈ riemannRochSpace (A + B)

The product of a section of L(A) and a section of L(B) is a section of L(A + B). The pole orders of a product add, as do the coefficients of its bounding divisors.

theorem TauCeti.Divisor.ord_eq_neg_coeff_of_not_mem_sub_ofPoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {P : Place k F} {z : F} (hz : z ∈ riemannRochSpace D) (hzsub : z ∉ riemannRochSpace (D - AlgebraicGeometry.WeilDivisor.ofPoint P)) : P.ord z = -AlgebraicGeometry.WeilDivisor.coeff D P

A section of L(D) outside L(D-P) has order exactly -D(P) at P.

The two ends of the divisor order

theorem TauCeti.mem_riemannRochSpace_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {f : F} : f ∈ riemannRochSpace 0 ↔ f ∈ algebraicClosure k F

Stichtenoth, Lemma 1.4.7(a), without a hypothesis on the constant field: the functions with no poles at all are exactly the constants algebraicClosure k F.

theorem TauCeti.riemannRochSpace_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : riemannRochSpace 0 = Subalgebra.toSubmodule (algebraicClosure k F).toSubalgebra

Stichtenoth, Lemma 1.4.7(a), as an equality of k-subspaces of F: L(0) = algebraicClosure k F.

theorem TauCeti.riemannRochSpace_zero_of_isIntegrallyClosedIn {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : riemannRochSpace 0 = (Algebra.linearMap k F).range

Stichtenoth, Lemma 1.4.7(a): over an exact constant field, L(0) = k.

theorem TauCeti.riemannRochSpace_eq_bot_of_lt_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : D < 0) : riemannRochSpace D = ⊥

Stichtenoth, Lemma 1.4.7(b): a divisor that is negative — everywhere at most zero, and somewhere strictly negative — has no functions at all. A nonzero f ∈ L(D) would have no pole, hence be a constant, hence have div f = 0, contradicting D < 0.

The one-place estimate

theorem TauCeti.finiteDimensional_riemannRochSpace_add_ofPoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) (P : Place k F) (h : FiniteDimensional k ↥(riemannRochSpace D)) : FiniteDimensional k ↥(riemannRochSpace (D + AlgebraicGeometry.WeilDivisor.ofPoint P))

Adding one place to a divisor keeps its Riemann–Roch space finite-dimensional.

theorem TauCeti.finrank_riemannRochSpace_add_ofPoint_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) (P : Place k F) (h : FiniteDimensional k ↥(riemannRochSpace D)) : Module.finrank k ↥(riemannRochSpace (D + AlgebraicGeometry.WeilDivisor.ofPoint P)) ≤ Module.finrank k ↥(riemannRochSpace D) + P.degree

Stichtenoth, Lemma 1.4.8, in its one-place form: passing from D to D + P raises the dimension of the Riemann–Roch space by at most deg P. The proof embeds the quotient L(D + P) / L(D) in the residue field of P by evaluating t · f at P, for t a function of order D P + 1 there.

Finite-dimensionality

theorem TauCeti.Divisor.dim_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : dim 0 = Module.finrank k ↥(algebraicClosure k F)

ℓ(0) = [algebraicClosure k F : k]: the functions without poles are the constants.

theorem TauCeti.Divisor.dim_zero_eq_finrank_of_isIntegrallyClosedIn {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {k' : Type u_3} [Field k'] [Algebra k k'] [Algebra k' F] [IsScalarTower k k' F] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F) (hex : IsIntegrallyClosedIn k' F) : dim 0 = Module.finrank k k'

If k' is the exact field of constants of a function field F / k, then ℓ(0) is the degree of k' / k.

theorem TauCeti.finiteDimensional_riemannRochSpace_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : FiniteDimensional k ↥(riemannRochSpace 0)

L(0) = algebraicClosure k F is finite-dimensional: the constants form a finite extension of k (Stichtenoth, Corollary 1.1.16).

theorem TauCeti.finiteDimensional_riemannRochSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : FiniteDimensional k ↥(riemannRochSpace D)

Stichtenoth, Proposition 1.4.9: the Riemann–Roch space of any divisor is finite-dimensional over the constants. No hypothesis on the constant field is needed here: the constants algebraicClosure k F form a finite extension of k and L(0) = algebraicClosure k F, and the estimate walking up from 0 to D⁺ is hypothesis-free.

theorem TauCeti.Divisor.dim_eq_zero_iff_riemannRochSpace_eq_bot {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : D.dim = 0 ↔ riemannRochSpace D = ⊥

The Riemann–Roch dimension is zero exactly when the Riemann–Roch space is zero.

theorem TauCeti.Divisor.one_le_dim_iff_riemannRochSpace_ne_bot {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : 1 ≤ D.dim ↔ riemannRochSpace D ≠ ⊥

The Riemann–Roch dimension is positive exactly when the Riemann–Roch space is nonzero.

theorem TauCeti.Divisor.dim_mono {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : D.dim ≤ E.dim

ℓ is monotone in the divisor (Stichtenoth, Lemma 1.4.8, first part).

theorem TauCeti.Divisor.dim_le_dim_add_degree_sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : ↑E.dim ≤ ↑D.dim + (degree E - degree D)

Stichtenoth, Lemma 1.4.8: enlarging a divisor raises ℓ by at most the increase in degree. Stichtenoth states this as dim (L(E)/L(D)) ≤ deg E - deg D; the two forms agree because L(D) is finite-dimensional.

theorem TauCeti.finrank_quotient_riemannRochSpace_le_degree_sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : ↑(Module.finrank k (↥(riemannRochSpace E) ⧸ (riemannRochSpace D).submoduleOf (riemannRochSpace E))) ≤ Divisor.degree E - Divisor.degree D

Stichtenoth, Lemma 1.4.8 in the quotient form Stichtenoth states it in: for D ≤ E the quotient L(E) / L(D) has dimension at most deg E - deg D. Inside L(E) the subspace L(D) is the trace Submodule.submoduleOf of the inclusion TauCeti.riemannRochSpace_mono; the arithmetic form of the same bound is TauCeti.Divisor.dim_le_dim_add_degree_sub.

theorem TauCeti.rank_quotient_riemannRochSpace_add_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : Module.rank k (↥(riemannRochSpace E) ⧸ (riemannRochSpace D).submoduleOf (riemannRochSpace E)) + ↑D.dim = ↑E.dim

Lemma 1.4.8 as an exact count of ranks: for D ≤ E the rank of the quotient L(E) / L(D) is ℓ(E) - ℓ(D), stated without subtraction as

rank (L(E)/L(D)) + ℓ(D) = ℓ(E).

This is the Module.rank-valued companion of TauCeti.finrank_quotient_riemannRochSpace_le_degree_sub, for use where the ambient module is not yet known to be finite-dimensional.

theorem TauCeti.Divisor.dim_le_degree_posPart_add_finrank {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : ↑D.dim ≤ degree D⁺ + ↑(Module.finrank k ↥(algebraicClosure k F))

Stichtenoth, Proposition 1.4.9, with the bound for a general constant field: ℓ(D) ≤ deg D⁺ + [algebraicClosure k F : k].

theorem TauCeti.Divisor.dim_le_degree_posPart_add_one {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) : ↑D.dim ≤ degree D⁺ + 1

Stichtenoth, Proposition 1.4.9: over an exact constant field the Riemann–Roch space of D has dimension at most deg D⁺ + 1. In particular ℓ(D) ≤ deg D + 1 for effective D.

theorem TauCeti.Divisor.dim_zero_of_isIntegrallyClosedIn {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : dim 0 = 1

Over an exact constant field ℓ(0) = 1: the only functions without poles are the constants.

theorem TauCeti.Divisor.dim_eq_zero_of_lt_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : D < 0) : D.dim = 0

ℓ(D) = 0 for a negative divisor (Stichtenoth, Lemma 1.4.7(b)).