Riemann-Roch for graphs

The Riemann-Roch theorem for graphs and its main corollaries, following [Corry-Perkinson], Chapter 5.

• riemann_roch_for_graphs: The Riemann-Roch theorem, $r(D) - r(K_G - D) = \deg(D) - g + 1$ ([Corry-Perkinson], Theorem 5.9).
• maximal_unwinnable_symmetry: $D$ is maximal unwinnable iff $K_G - D$ is ([Corry-Perkinson], Corollary 5.11).
• clifford_theorem: If $r(D) \geq 0$ and $r(K_G - D) \geq 0$, then $r(D) \leq \deg(D)/2$ ([Corry-Perkinson], Corollary 5.13).
• riemann_roch_deg_to_rank_corollary: Nonspecial range results ([Corry-Perkinson], Corollary 5.14).

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) - g + 1$. This is [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. This is [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 \deg(D)/2$. This is [Corry-Perkinson], Corollary 5.13.

theorem riemann_roch_deg_to_rank_corollary {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)

Nonspecial range: (1) $\deg(D) < 0 \Rightarrow r(D) = -1$; (2) $0 \leq \deg(D) \leq 2g-2 \Rightarrow r(D) \leq \deg(D)/2$; (3) $\deg(D) > 2g-2 \Rightarrow r(D) = \deg(D) - g$. This is [Corry-Perkinson], Corollary 5.14.

Gonality

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

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

Equations

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

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

gonality_geq G k means that no divisor of degree < 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 gonality of a connected graph is the smallest degree of a divisor of rank at least 1.

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

Conjectures

Below are some conjectures and theorems that have not been formalized at the time of this writing, as far as we are aware.

def gonality_conjecture_existence (g : ℕ) : Prop

The existence version of the gonality conjecture: for every $g \ge 0$, there exists a connected graph of genus $g$ with gonality exactly $\lfloor \frac12 (g+3) \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 tropcial proof of the Brill--Noether Theroem, but we are not aware of a formalization of this result.

Equations

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

def brill_noether_general_existence {G : CFGraph} (g : ℕ) : Prop

The statement that in a given genus $g$, there exists a Brill--Noether general graph. That is, a graph with no degree $d$ divisors of rank $r$ for which $\rho = g - (r+1)(g-d+r) < 0$. This is a slightly strengthened form of a conjecuture posed in M. Baker, Specialization of linear series 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 Theroem, 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 gonality_conjecture {G : CFGraph} (h_conn : graph_connected G) : Prop

The gonality conjecture for finite graphs: every genus $g$ connected graph has gonality at most $\lfloor \frac12 (g+3) \rfloor$. This is an open problem. Posted in M. Baker, 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 genus $g$ connected graph, and any $r, d$ with $\rho = g - (r+1)(g-d+r) \ge 0$, there exists a degree $d$ divisor of rank at least $r$. This is an open problem. Posed in M. Baker, Specialization of linear series from curves to graphs, Conjecture 3.9(1).

Equations

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