Maximal superstable configurations and maximal unwinnable divisors

This section establishes the correspondence between maximal superstable configurations and maximal unwinnable divisors:

• A superstable configuration $c$ is maximal if and only if $\deg(c) = g$ (maximal_superstable_config_prop).
• A divisor $D$ is maximal unwinnable if and only if its canonical $q$-reduced representative has the form $c-q$, with $c$ the associated maximal superstable configuration (maximal_unwinnable_char).
• Every maximal unwinnable divisor has degree $g - 1$ (maximal_unwinnable_deg).

noncomputable def qReducedRep {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : CFDiv G

The chosen unique $q$-reduced representative of the linear equivalence class of $D$.

Equations

• qReducedRep h_conn q D = Classical.choose ⋯

noncomputable def qReducedConfig {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : Config G q

The configuration obtained from the canonical $q$-reduced representative of $D$ by zeroing out the chips at $q$.

Equations

• qReducedConfig h_conn q D = toConfig { D := qReducedRep h_conn q D, h_eff := ⋯ }

theorem superstable_of_divisor {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : ∃ (c : Config G q) (k : ℤ), linear_equiv G D (c.chips + k • one_chip q) ∧ superstable G q c

Every divisor $D$ is linearly equivalent to $c+kq$ for some superstable configuration $c$ and integer $k$.

See: Corry-Perkinson, Remark 3.14.

theorem superstable_of_divisor_negative_k (G : CFGraph) (q : G.V) (D : CFDiv G) : ¬winnable G D → ∀ (c : Config G q) (k : ℤ), linear_equiv G D (c.chips + k • one_chip q) → superstable G q c → k < 0

If $D$ is unwinnable and $D \sim c + k \cdot q$ for a superstable $c$, then $k < 0$.

theorem winnable_of_deg_ge_genus {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : deg D ≥ genus G → winnable G D

A divisor of degree at least $g$ is winnable.

theorem maximal_unwinnable_char {G : CFGraph} (h_conn : graph_connected G) (q : G.V) (D : CFDiv G) : maximal_unwinnable G D ↔ maximal_superstable G (qReducedConfig h_conn q D) ∧ qReducedRep h_conn q D = (qReducedConfig h_conn q D).chips - one_chip q

A divisor $D$ is maximal unwinnable if and only if its canonical $q$-reduced representative has the form $c-q$, with $c$ the associated maximal superstable configuration.

See: Corry-Perkinson, Corollary 4.9(2), in canonical form.

theorem maximal_unwinnable_deg {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : maximal_unwinnable G D → deg D = genus G - 1

A maximal unwinnable divisor has degree $g - 1$, computed from its canonical $q$-reduced representative and canonical configuration.

See: Corry-Perkinson, Corollary 4.9(4).

theorem acyclic_orientation_maximal_unwinnable_correspondence_and_degree {G : CFGraph} (h_conn : graph_connected G) (q : G.V) : (Function.Injective fun (O : { O : CFOrientation G // is_acyclic G O ∧ is_source G O q }) (v : G.V) => indeg G (↑O) v - if v = q then 1 else 0) ∧ ∀ (D : CFDiv G), maximal_unwinnable G D → deg D = genus G - 1

The map sending an acyclic orientation with source $q$ to the divisor $v \mapsto \operatorname{indeg}(v) - \delta_{v,q}$ is injective, and every maximal unwinnable divisor has degree $g - 1$. The divisor used here differs from $D(\mathcal{O})$ by a fixed divisor, so injectivity is equivalent.

See: Corry-Perkinson, Corollary 4.9(3) for the injectivity claim.

Moderator divisors

Following terminology of Mikhalkin and Zharkov, a moderator is the divisor $D(\mathcal{O})$ of an acyclic orientation $\mathcal{O}$. Moderators encapsulate the key duality in the proof of Riemann-Roch: reversing the orientation carries $D(\mathcal{O})$ to $K_G - D(\mathcal{O})$.

def is_moderator {G : CFGraph} (D : CFDiv G) : Prop

A moderator is a divisor of the form $D(\mathcal{O})$ for some acyclic orientation $\mathcal{O}$.

Equations

• is_moderator D = ∃ (O : CFOrientation G), is_acyclic G O ∧ D = ordiv G O

theorem moderator_symmetry {G : CFGraph} (D : CFDiv G) : is_moderator D → is_moderator (canonical_divisor G - D)

If $D$ is a moderator, then so is $K_G - D$ (via the reverse orientation). This is the key duality in the proof of Riemann-Roch.

theorem moderator_degree {G : CFGraph} {D : CFDiv G} (h : is_moderator D) : deg D = genus G - 1

Moderators have degree $g-1$.

theorem unwinnable_of_moderator {G : CFGraph} {D : CFDiv G} (h : is_moderator D) : ¬winnable G D

Moderators are unwinnable.

theorem moderator_of_unwinnable {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) (unwin : ¬winnable G D) : ∃ (M : CFDiv G) (H : CFDiv G), is_moderator M ∧ effective H ∧ linear_equiv G M (D + H)

For every unwinnable divisor $D$, there exist a moderator $M$ and an effective divisor $H$ with $M \sim D + H$.

The main Riemann-Roch inequality

rank_degree_inequality establishes the strict inequality $$\deg(D) - g < r(D) - r(K_G - D),$$ which is the main step toward the Riemann-Roch theorem for graphs. The proof chooses an effective divisor $E$ of degree $r(D)+1$ with $D-E$ unwinnable, writes $M \sim (D-E)+F$ for a moderator $M$ and effective divisor $F$ (moderator_of_unwinnable), and then dualizes via moderator_symmetry to bound $r(K_G - D)$ by $\deg(F)$.

theorem rank_degree_inequality {G : CFGraph} (h_conn : graph_connected G) (D : CFDiv G) : deg D - genus G < rank G D - rank G (canonical_divisor G - D)

The strict Riemann-Roch inequality: $\deg(D) - g < r(D) - r(K_G - D)$.