Riemann-Roch for graphs

This file contains 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 rank_subadditive (G : CFGraph) (D D' : CFDiv G) (h_D : rank G D ≥ 0) (h_D' : rank G D' ≥ 0) : rank G (D + D') ≥ rank G D + rank G D'

Rank of divisors is subadditive.

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.

theorem one_le_of_gonality_leq {G : CFGraph} {k : ℤ} (h_gon : gonality_leq G k) : 1 ≤ k

Any degree realizing gonality_leq is at least 1.

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}

theorem gonality_le_genus_add_one {G : CFGraph} (h_conn : graph_connected G) : gonality h_conn ≤ genus G + 1

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

theorem gonality_ge_one {G : CFGraph} (h_conn : graph_connected G) : 1 ≤ gonality h_conn

The gonality of a connected graph is at least 1.

@[simp]

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