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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : 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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D D' : CFDiv V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] {G : CFGraph V} (h_conn : graph_connected G) (D : CFDiv V) : (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.