Riemann-Roch for graphs

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

See: Corry-Perkinson, Chapter 5.

theorem riemann_roch_for_graphs {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : rank G D - rank G (canonical_divisor 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 maximal_unwinnable_symmetry {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : maximal_unwinnable G D ↔ maximal_unwinnable G (canonical_divisor G - D)

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

See: Corry-Perkinson, Corollary 5.11.

theorem clifford_theorem {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) (h_D : rank G D ≥ 0) (h_KD : rank G (canonical_divisor 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 rank_nonspecial_range {G : CFGraph} (h_conn : graph_connected 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 gonality_leq (G : CFGraph) (k : ℤ) : Prop

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

Equations

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

def gonality_geq (G : CFGraph) (k : ℤ) : Prop

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

Equations

• gonality_geq G k = ∀ l < k, ¬gonality_leq G l

theorem gonality_leq_genus_add_one {G : CFGraph} (h_conn : graph_connected G) : gonality_leq G (genus G + 1)

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

noncomputable def gonality {G : CFGraph} (h_conn : graph_connected G) : ℤ

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

Equations

• gonality h_conn = sInf {k : ℤ | gonality_leq G k}

@[simp]

theorem gonality_geq_iff {G : CFGraph} (h_conn : graph_connected G) (k : ℤ) : gonality_geq G k ↔ gonality h_conn ≥ k

The relation gonality_geq 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 max_gonality_existence (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

• max_gonality_existence g = ∃ (G : CFGraph) (h_conn : graph_connected G) (_ : genus G = ↑g), gonality h_conn = (↑g + 3) / 2

def brill_noether_general_existence (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

• brill_noether_general_existence g = ∃ (G : CFGraph) (_ : graph_connected G) (_ : genus G = g), ∀ (D : CFDiv G), (rank G D + 1) * (rank G (canonical_divisor G - D) + 1) ≤ g

def gonality_conjecture {G : CFGraph} (h_conn : graph_connected 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

• gonality_conjecture h_conn = (gonality h_conn ≤ (genus G + 3) / 2)

def brill_noether_conjecture {G : CFGraph} (h_conn : graph_connected 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

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