Riemann–Roch spaces and principal divisors

The Riemann–Roch space L(D) of a divisor of an algebraic function field F / k is defined by a pole bound; the divisor of a function turns that bound into the single inequality div f + D ≥ 0. This file reads L(D) through the principal-divisor homomorphism TauCeti.Divisor.principal: it gives the divisor form of membership, and proves that multiplication by a nonzero function z is a k-linear isomorphism L(A) ≅ L(A - div z), so that ℓ depends only on the linear equivalence class of a divisor. It is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definition 1.4.4 and Lemma 1.4.6.

Main results

• TauCeti.mem_riemannRochSpace_units_iff: z ∈ L(D) is div z + D ≥ 0, the divisor form of the pole bound defining L(D).
• TauCeti.riemannRochSpaceEquivSubPrincipal: Stichtenoth, Lemma 1.4.6 — multiplication by z is a k-linear isomorphism L(A) ≅ L(A - div z); hence TauCeti.Divisor.dim_eq_of_linearlyEquivalent, ℓ is an invariant of the linear equivalence class of a divisor.
• TauCeti.Divisor.dim_principal: the dimension of a principal divisor is the degree of the full constant field over k.
• TauCeti.Divisor.eq_of_linearlyEquivalent_of_dim_eq_dim_zero: a divisor class with ℓ(D) = ℓ(0) contains at most one effective divisor (Remark 1.4.5).
• TauCeti.riemannRochSpace_ne_bot_iff: L(D) ≠ 0 exactly when D is linearly equivalent to an effective divisor (Remark 1.4.5(b)).

None of this needs the product formula deg (div z) = 0 (Stichtenoth, Theorem 1.4.11), which is separate work; every statement here is independent of it.

References

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

theorem TauCeti.mem_riemannRochSpace_units_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {z : Fˣ} : ↑z ∈ riemannRochSpace D ↔ 0 ≤ Divisor.principal hF z + D

The divisor form of membership in L(D): a nonzero function lies in L(D) exactly when div f + D is effective, which is how Stichtenoth states Definition 1.4.4.

theorem TauCeti.mul_mem_riemannRochSpace_sub_principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {A : Divisor k F} {f : F} (hf : f ∈ riemannRochSpace A) : ↑z * f ∈ riemannRochSpace (A - Divisor.principal hF z)

Multiplying by z moves L(A) into L(A - div z): the poles of z * f are bounded by those of f together with the poles z contributes.

noncomputable def TauCeti.riemannRochSpaceEquivSubPrincipal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (A : Divisor k F) : ↥(riemannRochSpace A) ≃ₗ[k] ↥(riemannRochSpace (A - Divisor.principal hF z))

Stichtenoth, Lemma 1.4.6: multiplication by a nonzero function z is a k-linear isomorphism L(A) ≅ L(A - div z).

This is the whole content of the invariance of ℓ under linear equivalence: any two linearly equivalent divisors differ by a principal divisor, and this isomorphism handles that difference. It needs no product formula, so it is available before deg (div z) = 0.

Equations

• TauCeti.riemannRochSpaceEquivSubPrincipal hF z A = ((Units.mulLeftLinearEquiv k F) z).ofSubmodules (TauCeti.riemannRochSpace A) (TauCeti.riemannRochSpace (A - TauCeti.Divisor.principal hF z)) ⋯

@[simp]

theorem TauCeti.riemannRochSpaceEquivSubPrincipal_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (A : Divisor k F) (f : ↥(riemannRochSpace A)) : ↑((riemannRochSpaceEquivSubPrincipal hF z A) f) = ↑z * ↑f

The Riemann–Roch-space equivalence acts by multiplication by z.

@[simp]

theorem TauCeti.riemannRochSpaceEquivSubPrincipal_symm_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (A : Divisor k F) (f : ↥(riemannRochSpace (A - Divisor.principal hF z))) : ↑((riemannRochSpaceEquivSubPrincipal hF z A).symm f) = ↑z⁻¹ * ↑f

The inverse Riemann–Roch-space equivalence acts by multiplication by z⁻¹.

theorem TauCeti.Divisor.dim_sub_principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (A : Divisor k F) : (A - principal hF z).dim = A.dim

ℓ(A - div z) = ℓ(A): the dimension of a Riemann–Roch space is unchanged by subtracting a principal divisor.

theorem TauCeti.Divisor.dim_eq_of_linearlyEquivalent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {A B : Divisor k F} (h : (Place.orderSystem hF).LinearlyEquivalent A B) : A.dim = B.dim

ℓ is an invariant of the divisor class (Stichtenoth, Lemma 1.4.6): linearly equivalent divisors have Riemann–Roch spaces of the same dimension.

@[simp]

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

The Riemann–Roch dimension of a principal divisor is the degree of the full constant field.

theorem TauCeti.Divisor.dim_principal_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) (z : Fˣ) : (principal hF z).dim = 1

Over an exact constant field, the Riemann–Roch dimension of a principal divisor is one.

theorem TauCeti.Divisor.eq_of_linearlyEquivalent_of_dim_eq_dim_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (hD : 0 ≤ D) (hE : 0 ≤ E) (hdim : D.dim = dim 0) (h : (Place.orderSystem hF).LinearlyEquivalent D E) : D = E

A divisor class with ℓ(D) = ℓ(0) contains at most one effective divisor (Stichtenoth, Remark 1.4.5): the only effective divisor linearly equivalent to an effective D whose Riemann–Roch space has the dimension of the constant space is D itself, so the complete linear system of D is the singleton {D}.

theorem TauCeti.Divisor.eq_of_linearlyEquivalent_of_dim_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (hD : 0 ≤ D) (hE : 0 ≤ E) (hdim : D.dim = 1) (h : (Place.orderSystem hF).LinearlyEquivalent D E) : D = E

A divisor class with ℓ(D) = 1 contains at most one effective divisor.

theorem TauCeti.riemannRochSpace_ne_bot_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} : riemannRochSpace D ≠ ⊥ ↔ ∃ (D' : Divisor k F), 0 ≤ D' ∧ (Place.orderSystem hF).LinearlyEquivalent D D'

A Riemann–Roch space is nonzero exactly when its divisor is linearly equivalent to an effective divisor (Stichtenoth, Remark 1.4.5(b)). A nonzero f ∈ L(D) makes div f + D effective and equivalent to D; conversely, if D - D' is the divisor of z with D' effective, then z⁻¹ is a nonzero element of L(D).

theorem TauCeti.mem_riemannRochSpace_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : ↑z ∈ riemannRochSpace (Divisor.poles hF z)

A nonzero function lies in the Riemann–Roch space of its pole divisor.

theorem TauCeti.pow_mem_riemannRochSpace_zsmul_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (n : ℕ) : ↑z ^ n ∈ riemannRochSpace (↑n • Divisor.poles hF z)

The n-th power of a nonzero function has poles bounded by n times its pole divisor.

theorem TauCeti.pow_mem_riemannRochSpace_zsmul_poles_of_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) {i : ℕ} {m : ℤ} (h : ↑i ≤ m) : ↑z ^ i ∈ riemannRochSpace (m • Divisor.poles hF z)

z ^ i ∈ L(m · (z)_∞) whenever i ≤ m: in particular the powers 1, z, …, z^{n-1} of a nonzero function lie in L((n - 1) · (z)_∞).