The rank function

The rank of a divisor $D$ is the integer $r(D) \in \{-1, 0, 1, \ldots\}$ defined by $r(D) \geq k$ if and only if $D - E$ is winnable for every effective divisor $E$ of degree $k$. Equivalently, $r(D) \geq 0$ if and only if $D$ is winnable, and $r(D) = -1$ if and only if $D$ is unwinnable.

See: Corry-Perkinson, Section 5.1.

The rank is well-defined (rank_exists, rank_unique) and realized by the noncomputable rank function. Key properties established here include:

• rank_neg_one_iff_unwinnable: $r(D) = -1 \iff D$ is unwinnable.
• rank_nonneg_iff_winnable: $r(D) \geq 0 \iff D$ is winnable.
• rank_le_degree: $r(D) \leq \deg(D)$ for $r(D) \geq 0$.
• zero_divisor_rank: $r(0) = 0$.

A divisor $D$ is maximal unwinnable if it is unwinnable but $D + \delta_v$ is winnable for every vertex $v$. Such divisors arise in the proof of the Riemann-Roch theorem.

theorem winnable_equiv_winnable (G : CFGraph) (D1 D2 : CFDiv G) : winnable G D1 → linear_equiv G D1 D2 → winnable G D2

Winnability is preserved under linear equivalence.

def maximal_unwinnable (G : CFGraph) (D : CFDiv G) : Prop

A divisor is maximal unwinnable if it is unwinnable but adding a chip to any vertex makes it winnable.

Equations

• maximal_unwinnable G D = (¬winnable G D ∧ ∀ (v : G.V), winnable G (D + one_chip v))

theorem maximal_unwinnable_preserved (G : CFGraph) (D1 D2 : CFDiv G) : maximal_unwinnable G D1 → linear_equiv G D1 D2 → maximal_unwinnable G D2

Being maximal unwinnable is preserved under linear equivalence.

def eff_of_degree (G : CFGraph) (k : ℤ) : Set (CFDiv G)

The set of effective divisors of degree $k$.

This is used to define rank_geq: the relation $r(D) \ge k$ means that $D-E$ is winnable for every effective divisor $E$ of degree $k$.

Equations

• eff_of_degree G k = {E : CFDiv G | effective E ∧ deg E = k}

def rank_geq (G : CFGraph) (D : CFDiv G) (k : ℤ) : Prop

The relation $r(D) \ge k$: the game remains winnable after removing any effective divisor of degree $k$.

Equations

• rank_geq G D k = ∀ E ∈ eff_of_degree G k, winnable G (D - E)

def rank_eq (G : CFGraph) (D : CFDiv G) (r : ℤ) : Prop

The relation $r(D)=r$: rank_geq G D r holds, but rank_geq G D (r+1) does not.

Equations

• rank_eq G D r = (rank_geq G D r ∧ ¬rank_geq G D (r + 1))

theorem winnable_of_effective (G : CFGraph) (D : CFDiv G) (h_eff : effective D) : winnable G D

Every effective divisor is winnable (take $D' = D$ in the definition).

theorem winnable_add_winnable (G : CFGraph) (D1 D2 : CFDiv G) (h_winnable1 : winnable G D1) (h_winnable2 : winnable G D2) : winnable G (D1 + D2)

The sum of two winnable divisors is winnable.

theorem rank_le_degree (G : CFGraph) (D : CFDiv G) (r : ℤ) : r ≥ 0 → rank_geq G D r → r ≤ deg D

If $r(D) \ge r$ for some $r \ge 0$, then $r \le \deg(D)$.

In particular, rank G D ≤ deg D when rank G D ≥ 0.

theorem lt_of_rank_geq_not (G : CFGraph) (D : CFDiv G) (r1 r2 : ℤ) : rank_geq G D r1 → ¬rank_geq G D r2 → r1 < r2

If $r(D) \ge r_1$ holds but $r(D) \ge r_2$ does not, then $r_1 < r_2$.

theorem rank_nonneg_iff_winnable (G : CFGraph) (D : CFDiv G) : rank_geq G D 0 ↔ winnable G D

The inequality $r(D)\ge 0$ holds if and only if $D$ is winnable.

theorem rank_exists (G : CFGraph) (D : CFDiv G) : ∃ (r : ℤ), rank_eq G D r

Every divisor has a well-defined rank: there exists an integer $r$ with $r(D)=r$.

noncomputable def rank (G : CFGraph) (D : CFDiv G) : ℤ

The rank function for divisors.

Equations

• rank G D = Classical.choose ⋯

theorem rank_geq_iff (G : CFGraph) (D : CFDiv G) (k : ℤ) : rank_geq G D k ↔ rank G D ≥ k

The relation rank_geq G D k is equivalent to the inequality rank G D ≥ k.

theorem winnable_iff_exists_effective (G : CFGraph) (D : CFDiv G) : winnable G D ↔ ∃ (D' : CFDiv G), effective D' ∧ linear_equiv G D D'

A divisor is winnable if and only if it is linearly equivalent to an effective divisor.

theorem rank_get_effective (G : CFGraph) (D : CFDiv G) : ∃ (E : CFDiv G), effective E ∧ deg E = rank G D + 1 ∧ ¬winnable G (D - E)

There is an effective divisor $E$ of degree $r(D)+1$ such that $D-E$ is not winnable.

theorem rank_neg_one_iff_unwinnable (G : CFGraph) (D : CFDiv G) : rank G D = -1 ↔ ¬winnable G D

A divisor has rank $-1$ if and only if it is not winnable.

theorem rank_neg_one_of_deg_neg (G : CFGraph) (D : CFDiv G) (h_deg : deg D < 0) : rank G D = -1

A divisor of negative degree has rank $-1$, i.e. is unwinnable.

theorem rank_geq_neg_one (G : CFGraph) (D : CFDiv G) : rank G D ≥ -1

The rank of a divisor is at least $-1$.

theorem rank_neg_one_of_not_nonneg (G : CFGraph) (D : CFDiv G) (h_not_nonneg : ¬rank G D ≥ 0) : rank G D = -1

If the rank is not nonnegative, then it is $-1$.

theorem zero_divisor_rank (G : CFGraph) : rank G 0 = 0

The rank of the zero divisor is zero.