Riemann-Roch for graphs

The Riemann-Roch theorem for graphs and its main corollaries.

See: Corry-Perkinson, Chapter 5.

theorem ChipFiring.riemann_roch_for_graphs {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) : rank G D - rank G (canonicalDivisor G - D) = deg D - genus G + 1

Riemann-Roch theorem for graphs: $r(D) - r(K_G - D) = \deg(D) + 1 - g$.

See: Corry-Perkinson, Theorem 5.9.

theorem ChipFiring.maximal_unwinnable_symmetry {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) : maximalUnwinnable G D ↔ maximalUnwinnable G (canonicalDivisor G - D)

$D$ is maximal unwinnable if and only if $K_G - D$ is maximal unwinnable.

See: Corry-Perkinson, Corollary 5.11.

theorem ChipFiring.clifford_theorem {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) (h_D : rank G D ≥ 0) (h_KD : rank G (canonicalDivisor G - D) ≥ 0) : ↑(rank G D) ≤ ↑(deg D) / 2

Clifford's theorem: If $r(D) \geq 0$ and $r(K_G - D) \geq 0$, then $r(D) \leq \frac12 \deg(D)$.

See: Corry-Perkinson, Corollary 5.13.

theorem ChipFiring.rank_nonspecial_range {G : CFGraph} (h_conn : graphConnected G) (D : CFDiv G) : (deg D < 0 → rank G D = -1) ∧ (0 ≤ ↑(deg D) ∧ ↑(deg D) ≤ 2 * ↑(genus G) - 2 → ↑(rank G D) ≤ ↑(deg D) / 2) ∧ (deg D > 2 * genus G - 2 → rank G D = deg D - genus G)

The rank of a divisor in terms of its degree:

• $\deg(D) < 0 \Rightarrow r(D) = -1$
• $0 \leq \deg(D) \leq 2g-2 \Rightarrow r(D) \leq \deg(D)/2$
• $\deg(D) > 2g-2 \Rightarrow r(D) = \deg(D) - g$.

See: Corry-Perkinson, Corollary 5.14.

Gonality

The Riemann-Roch theorem provides some basic information about the (divisorial) gonality of a graph.

def ChipFiring.gonalityLeq (G : CFGraph) (k : ℤ) : Prop

The relation $\operatorname{gon}(G) \le k$: there exists a divisor of degree $k$ with rank at least $1$.

Equations

• ChipFiring.gonalityLeq G k = ∃ (D : ChipFiring.CFDiv G), ChipFiring.rank G D ≥ 1 ∧ ChipFiring.deg D = k

def ChipFiring.gonalityGeq (G : CFGraph) (k : ℤ) : Prop

The relation $\operatorname{gon}(G) \ge k$: no divisor of degree less than $k$ has rank at least $1$.

Equations

• ChipFiring.gonalityGeq G k = ∀ l < k, ¬ChipFiring.gonalityLeq G l

theorem ChipFiring.gonality_leq_genus_add_one {G : CFGraph} (h_conn : graphConnected G) : gonalityLeq G (genus G + 1)

A connected graph has gonality at most $g+1$, where $g$ is its genus.

noncomputable def ChipFiring.gonality {G : CFGraph} (_h_conn : graphConnected G) : ℤ

The (divisorial) gonality of a connected graph is the smallest degree of a divisor of rank at least one.

Equations

• ChipFiring.gonality _h_conn = sInf {k : ℤ | ChipFiring.gonalityLeq G k}

@[simp]

theorem ChipFiring.gonality_geq_iff {G : CFGraph} (h_conn : graphConnected G) (k : ℤ) : gonalityGeq G k ↔ gonality h_conn ≥ k

The relation gonalityGeq G k is equivalent to the inequality gonality h_conn ≥ k.

Conjectures

This section records conjectures and theorems about gonality and Brill-Noether theory for graphs that have not been formalized here.

def ChipFiring.maxGonalityExistence (g : ℕ) : Prop

The existence of graphs with maximum gonality: for every $g \ge 0$, there exists a connected graph of genus $g$ with gonality exactly $\lfloor (g+3)/2 \rfloor$.

Posed by M. Baker in Specialization of linear systems from curves to graphs, Conjecture 3.10(2). This is proved by Cools-Draisma-Payne-Robeva in A tropical proof of the Brill-Noether theorem, and via a different construction by Hendrey in Sparse graphs of high gonality. We are not aware of a formalization of this result.

Equations

• ChipFiring.maxGonalityExistence g = ∃ (G : ChipFiring.CFGraph) (h_conn : ChipFiring.graphConnected G) (_ : ChipFiring.genus G = ↑g), ChipFiring.gonality h_conn = (↑g + 3) / 2

def ChipFiring.brillNoetherGeneralExistence (g : ℤ) : Prop

The statement that in a given genus $g$, there exists a Brill-Noether general graph: a graph with no divisor of degree $d$ and rank at least $r$ whenever $$ \rho = g - (r+1)(g-d+r) < 0. $$

The statement below uses the Riemann-Roch-equivalent form $$ (r(D)+1)(r(K_G-D)+1) \le g $$ for all divisors $D$, to avoid coercions between natural numbers and integers.

This is a slightly strengthened form of a conjecture posed in M. Baker, Specialization of linear systems from curves to graphs, namely Conjecture 3.9(2). It was proved by Cools-Draisma-Payne-Robeva in A tropical proof of the Brill-Noether theorem, but we are not aware of a formalization of this result.

Equations

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

def ChipFiring.gonalityConjecture {G : CFGraph} (h_conn : graphConnected G) : Prop

The gonality conjecture for finite graphs: every connected graph of genus $g$ has gonality at most $\lfloor (g+3)/2 \rfloor$.

This is an open problem, posed by Baker in Specialization of linear systems from curves to graphs, Conjecture 3.10(1).

Equations

• ChipFiring.gonalityConjecture h_conn = (ChipFiring.gonality h_conn ≤ (ChipFiring.genus G + 3) / 2)

def ChipFiring.brillNoetherConjecture {G : CFGraph} (_h_conn : graphConnected G) (r d : ℤ) : Prop

The Brill-Noether conjecture for finite graphs: for every connected graph of genus $g$ and integers $r,d$ with $$ \rho = g - (r+1)(g-d+r) \ge 0, $$ there exists a divisor of degree $d$ and rank at least $r$.

This is an open problem, posed in slightly different form by Baker in Specialization of linear systems from curves to graphs, Conjecture 3.9(1).

Equations

• ChipFiring.brillNoetherConjecture _h_conn r d = (0 ≤ ChipFiring.genus G - (r + 1) * (ChipFiring.genus G - d + r) → ∃ (D : ChipFiring.CFDiv G), ChipFiring.rank G D ≥ r ∧ ChipFiring.deg D = d)