Corollaries of Riemann–Roch

Standard consequences of the main theorem, including C5 (Clifford) and C6 (existence of non-special divisors).

theorem FunctionField.Chart.ell_canonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) : ell k K W = genus k K

C1: for a canonical divisor, ℓ(W) = g.

theorem FunctionField.Chart.deg_canonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) : deg k K W = 2 * ↑(genus k K) - 2

C2: deg W = 2g − 2.

theorem FunctionField.Chart.ell_eq_of_deg_ge (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) (hdeg : deg k K D ≥ 2 * ↑(genus k K) - 1) : ↑(ell k K D) = deg k K D + 1 - ↑(genus k K)

C3: if deg D ≥ 2g − 1 then ℓ(D) = deg D + 1 − g.

theorem FunctionField.Chart.indexOfSpecialty_eq_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) : ↑(indexOfSpecialty k K D) = ↑(ell k K (W - D))

C4: index-of-specialty language matches ℓ(W − D).

theorem FunctionField.Chart.indexOfSpecialty_eq_zero_of_large_deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : DivisorA k K) (hdeg : deg k K D ≥ 2 * ↑(genus k K) - 1) : indexOfSpecialty k K D = 0

The specialty index vanishes in degree at least 2g - 1.

theorem FunctionField.Chart.indexOfSpecialty_eq_zero_of_le_deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (c : ℤ), ∀ (D : DivisorA k K), c ≤ deg k K D → indexOfSpecialty k K D = 0

The specialty index vanishes above a uniform degree bound.

theorem FunctionField.Chart.exists_effective_add_principal_of_ell_pos (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (hD : 0 < ell k K D) : ∃ (x : Kˣ), IsEffective k K (D + (principalDivisorA k K) (Additive.ofMul x))

A positive-dimensional Riemann–Roch space supplies an effective representative of the divisor's linear-equivalence class.

theorem FunctionField.Chart.RRspace_inf (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) : RRspace k K (D ⊓ E) = RRspace k K D ⊓ RRspace k K E

Riemann–Roch spaces preserve infima of divisors.

theorem FunctionField.Chart.RRspace_sup_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) : RRspace k K D ⊔ RRspace k K E ≤ RRspace k K (D ⊔ E)

The sum of two Riemann–Roch spaces lies in the space of the supremum divisor.

theorem FunctionField.Chart.ell_submodular (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) : ell k K D + ell k K E ≤ ell k K (D ⊔ E) + ell k K (D ⊓ E)

Riemann–Roch dimension is submodular on the divisor lattice.

theorem FunctionField.Chart.exists_minimal_RRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (A : DivisorA k K) (hA : 0 < ell k K A) : ∃ D₀ ≤ A, RRspace k K D₀ = RRspace k K A ∧ ∀ (v : PlaceA k K), ell k K (D₀ - Finsupp.single v 1) < ell k K D₀

Every positive-dimensional complete linear system has a representative minimal under removing one copy of any place.

theorem FunctionField.Chart.exists_RRspace_avoiding (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Infinite k] (D₀ : DivisorA k K) (s : Finset (PlaceA k K)) (hdrop : ∀ v ∈ s, ell k K (D₀ - Finsupp.single v 1) < ell k K D₀) : ∃ (z : ↥(RRspace k K D₀)), ∀ v ∈ s, ↑z ∉ RRspace k K (D₀ - Finsupp.single v 1)

Over an infinite constant field, finitely many one-place drops from a minimal complete linear system can be avoided simultaneously.

theorem FunctionField.Chart.memRRspace_iff_neg_principalDivisor_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D : DivisorA k K} {f : K} (hf : f ≠ 0) : memRRspace k K D f ↔ ∀ (v : PlaceA k K), -((principalDivisorA k K) (Additive.ofMul (Units.mk0 f hf))) v ≤ D v

Membership of a nonzero function in L(D) expressed coefficientwise through its principal divisor.

theorem FunctionField.Chart.eq_algebraMap_of_mul_mem (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {D₀ B : DivisorA k K} (hB0 : B ≠ 0) {z x : K} (hz : memRRspace k K D₀ z) (havoid : ∀ v ∈ B.support, z ∉ RRspace k K (D₀ - Finsupp.single v 1)) (hx : memRRspace k K B x) (hmul : memRRspace k K D₀ (x * z)) : ∃ (c : k), x = (algebraMap k K) c

If multiplication by a section that is exact at every place in supp B creates no new poles, the other factor is constant.

theorem FunctionField.Chart.ell_add_ell_le_of_effective_minimal (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] [Infinite k] (D₀ B : DivisorA k K) (hB : IsEffective k K B) (hB0 : B ≠ 0) (hdrop : ∀ v ∈ B.support, ell k K (D₀ - Finsupp.single v 1) < ell k K D₀) : ell k K D₀ + ell k K B ≤ 1 + ell k K (D₀ + B)

Stichtenoth's key Clifford inequality for an effective nonzero second divisor and a first divisor minimal under one-place drops.

theorem FunctionField.Chart.ell_add_ell_le_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] [Infinite k] (A B : DivisorA k K) (hA : 0 < ell k K A) (hB : 0 < ell k K B) : ell k K A + ell k K B ≤ 1 + ell k K (A + B)

Stichtenoth Lemma 1.6.14 over an infinite full constant field.

theorem FunctionField.Chart.ell_add_ell_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (A B : DivisorA k K) (hA : 0 < ell k K A) (hB : 0 < ell k K B) : ell k K A + ell k K B ≤ 1 + ell k K (A + B)

Stichtenoth Lemma 1.6.14 over an arbitrary full constant field. This is the Riemann–Roch-space specialization of mul_finrank.

theorem FunctionField.Chart.clifford_of_ell_pos (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) (hℓD : 0 < ell k K D) (hℓW : 0 < ell k K (W - D)) : 2 * (↑(ell k K D) - 1) ≤ deg k K D

The core Clifford inequality: with W canonical, whenever both ℓ(D) and ℓ(W − D) are positive, 2(ℓ(D) − 1) ≤ deg D. The textbook degree bounds 0 ≤ deg D ≤ 2g − 2 are not required — positivity of both dimensions, the linear product bound, and Riemann–Roch suffice.

theorem FunctionField.Chart.clifford (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) (_hdeg₀ : 0 ≤ deg k K D) (_hdeg₁ : deg k K D ≤ 2 * ↑(genus k K) - 2) (hℓD : 0 < ell k K D) (hℓW : 0 < ell k K (W - D)) : 2 * (↑(ell k K D) - 1) ≤ deg k K D

C5 (Clifford): if 0 ≤ deg D ≤ 2g − 2 and both ℓ(D) and ℓ(W − D) are positive, then 2(ℓ(D) − 1) ≤ deg D. This is the conventional textbook statement; the degree hypotheses are kept for fidelity but are not needed for the inequality (see clifford_of_ell_pos).

theorem FunctionField.Chart.exists_nonspecial_divisor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (D : DivisorA k K), indexOfSpecialty k K D = 0

C6 (field-independent form): a divisor attaining the maximal defect is nonspecial. The stronger assertion that one can choose an effective divisor of degree g requires additional hypotheses on the constant field and is not valid over every field.