The Brill--Noether rank of a finite graph

Lim, Payne and Potashnik introduced the Brill--Noether rank w^r_d of a metric graph as a well-behaved substitute for dim W^r_d, which is not upper semicontinuous on the moduli space of metric graphs (arXiv:1106.5519, Definition 3.1):

w^r_d(Γ) is the largest integer k such that, for every effective divisor E of degree r + k, there exists a divisor D of degree d and rank at least r on Γ such that D - E is effective. If W^r_d(Γ) is empty, w^r_d(Γ) is -1.

Len extended the definition to weighted tropical curves and proved upper semicontinuity there (arXiv:1209.6309, §6). Both papers prove a specialization inequality dim W^r_d(X) ≤ w^r_d(Γ), from which LPP deduce w^r_d(Γ) ≥ min {ρ(g,r,d), g} for every metric graph — by transfer from algebraic geometry, never combinatorially.

This file records the discrete analogue, in which both E and D are supported on the vertices of a finite graph. Note the degree bookkeeping: w^r_d ≥ k tests effective divisors of degree r + k, not k. Consequently

• w^r_d(G) ≥ 0 is exactly Brill--Noether existence (bnRankGe_zero_iff_bnExists): a single divisor of rank at least r already absorbs every effective divisor of degree r, by the definition of rank. Nothing is gained at k = 0.
• w^r_d(G) ≥ 1 is genuinely more. It splits into a ramification half (E = 2•v) and a secant half (E = v + w, v ≠ w), and neither half implies the other in general.

Besides the definition and its basic reformulations, this file proves that the predicate is downward closed in k (bnRankGe_of_le), that it fails once the degree drops below r + k (not_bnRankGe_of_lt), and that it is invariant under an adjacency-preserving relabeling of vertices (Certificate.LaplacianEquiv.bnRankGe_iff). These combine into the numerical invariant bnRank, normalized as in Len to be -1 when W^r_d is empty.

The descent of this predicate along an odd subdivision lives in Utilities/Subdivision/SubdivisionChipDescent.lean and is not imported here.

The definition

def Utilities.BNRankGe (G : CFGraph) (r d k : ℤ) : Prop

BNRankGe G r d k is the discrete Brill--Noether rank inequality w^r_d(G) ≥ k of Lim--Payne--Potashnik and Len: every effective divisor E of degree r + k is contained, up to linear equivalence, in a divisor of degree d and rank at least r.

The literature says "E is contained in an effective divisor D of degree d and rank at least r"; since rank is a class invariant, that is the same as asking for D - E to be winnable, which is the form stated here. The containment form is recovered by bnRankGe_iff_contained.

Equations

• Utilities.BNRankGe G r d k = ∀ (E : CFDiv G), effective E → CFDiv.degree E = r + k → ∃ (D : CFDiv G), CFDiv.degree D = d ∧ rank G D ≥ r ∧ winnable G (D - E)

theorem Utilities.bnRankGe_iff_contained (G : CFGraph) (r d k : ℤ) : BNRankGe G r d k ↔ ∀ (E : CFDiv G), effective E → CFDiv.degree E = r + k → ∃ (D : CFDiv G), effective D ∧ CFDiv.degree D = d ∧ rank G D ≥ r ∧ effective (D - E)

The literal Lim--Payne--Potashnik phrasing: every effective E of degree r + k is contained in an effective divisor of degree d and rank at least r.

The rank-zero case is exactly Brill--Noether existence

theorem Utilities.bnRankGe_zero_iff_bnExists (G : CFGraph) (r d : ℤ) (hr : 0 ≤ r) : BNRankGe G r d 0 ↔ BNExists G r d

The k = 0 case is not new information. w^r_d(G) ≥ 0 says that every effective divisor of degree r can be absorbed, and that is precisely the definition of a divisor of rank at least r. So the Brill--Noether rank inequality at k = 0 is equivalent to plain Brill--Noether existence.

Degree slack

Brill--Noether existence one degree lower buys one unit of Brill--Noether rank for free: split E into a degree-r piece, absorbed by the rank of the smaller witness, and a degree-one remainder, simply added on.

theorem Utilities.bnRankGe_of_bnExists_pred (G : CFGraph) (r d : ℤ) (hr : 0 ≤ r) (hExists : BNExists G r (d - 1)) : BNRankGe G r d 1

If G carries a divisor of degree d - 1 and rank at least r, then w^r_d(G) ≥ 1.

Effective divisors of degree two

theorem Utilities.exists_chip_pair_of_effective_deg_two (G : CFGraph) (A : CFDiv G) (hEffective : effective A) (hDegree : CFDiv.degree A = 2) : ∃ (x : G.V) (y : G.V), A = oneChip x + oneChip y

An effective divisor of degree two is a sum of two vertex chips.

theorem Utilities.bnRankGe_one_of_bnExists_one_three (G : CFGraph) (hExists : BNExists G 1 3) : BNRankGe G 1 4 1

Gonality at most three already forces w^1_4(G) ≥ 1, whatever the genus. The open genus-five cases are therefore exactly the graphs of gonality four.

Monotonicity in the Brill--Noether rank parameter

theorem Utilities.bnRankGe_of_le {G : CFGraph} {r d k k' : ℤ} (_hk : 0 ≤ r + k') (hkk : k' ≤ k) (h : BNRankGe G r d k) : BNRankGe G r d k'

Downward closure in k. An effective divisor E' of degree r + k' is padded to degree r + k by heaping the missing k - k' chips on a single vertex; the residual of the padded divisor is winnable, hence so is the residual of E', which differs from it by an effective divisor.

The hypothesis 0 ≤ r + k' is not needed — below that range the statement is vacuous, since there are no effective divisors of negative degree — but it is kept in the interface, as every intended use supplies it.

theorem Utilities.not_bnRankGe_of_lt {G : CFGraph} {r d k : ℤ} (hr : 0 ≤ r) (hk : 0 ≤ k) (hdk : d < r + k) : ¬BNRankGe G r d k

The degree ceiling. A divisor of degree d cannot absorb an effective divisor of larger degree: the residual would be winnable of negative degree. Since hk guarantees that an effective divisor of degree r + k exists, the Brill--Noether rank inequality fails outright once d < r + k.

The numerical Brill--Noether rank

noncomputable def Utilities.bnRank (G : CFGraph) (r d : ℤ) : ℤ

The Brill--Noether rank w^r_d(G), normalized as in Len: it is -1 when W^r_d(G) is empty, and otherwise the largest k ≥ 0 for which the inequality BNRankGe G r d k holds. The supremum is attained because the set of such k is a nonempty set of integers bounded above by d - r (bnRankGe_iff_le_bnRank).

Equations

• Utilities.bnRank G r d = if Utilities.BNExists G r d then sSup {k : ℤ | 0 ≤ k ∧ Utilities.BNRankGe G r d k} else -1

theorem Utilities.bnRank_eq_neg_one_of_not_bnExists {G : CFGraph} {r d : ℤ} (hExists : ¬BNExists G r d) : bnRank G r d = -1

Len's normalization: an empty W^r_d has Brill--Noether rank -1.

theorem Utilities.bnRankGe_iff_le_bnRank {G : CFGraph} {r d k : ℤ} (hr : 0 ≤ r) (hk : 0 ≤ k) : BNRankGe G r d k ↔ k ≤ bnRank G r d

The defining property of bnRank. For nonnegative parameters the predicate BNRankGe is exactly the comparison k ≤ w^r_d(G).

theorem Utilities.bnRank_nonneg_iff {G : CFGraph} {r d : ℤ} (hr : 0 ≤ r) : 0 ≤ bnRank G r d ↔ BNExists G r d

Nonnegativity of the Brill--Noether rank is Brill--Noether existence.

Transport along an adjacency-preserving relabeling

theorem Utilities.Certificate.LaplacianEquiv.bnRankGe_of_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) {r d k : ℤ} (hRank : BNRankGe H r d k) : BNRankGe G r d k

The Brill--Noether rank inequality transports backwards along an adjacency-preserving vertex equivalence.

theorem Utilities.Certificate.LaplacianEquiv.bnRankGe_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (r d k : ℤ) : BNRankGe H r d k ↔ BNRankGe G r d k

The Brill--Noether rank inequality is unchanged by relabeling vertices.