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$ iff $D - E$ is winnable for every effective divisor $E$ of degree $k$ ([Corry-Perkinson], Section 5.1). Equivalently, $r(D) \geq 0$ iff $D$ is winnable, and $r(D) = -1$ iff $D$ is unwinnable.

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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D1 D2 : CFDiv V) : winnable G D1 → linear_equiv G D1 D2 → winnable G D2

Winnability is preserved under linear equivalence.

def maximal_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : 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 : V), winnable G (D + one_chip v))

theorem maximal_unwinnable_preserved {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D1 D2 : CFDiv V) : 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 {V : Type} [Fintype V] (D : CFDiv V) (k : ℤ) : Set (CFDiv V)

The set of effective divisors of degree k. Used to define rank_geq: rank G D ≥ k means D - E is winnable for every E in eff_of_degree D k.

Equations

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

theorem eff_of_degree_nonempty {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (D : CFDiv V) (k : ℕ) : k ≥ 0 → (eff_of_degree D ↑k).Nonempty

For any natural number k, the set of effective divisors of degree k is nonempty.

def rank_geq {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (k : ℤ) : Prop

A divisor D has rank ≥ k if the game is winnable after removing any k dollars

Equations

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

def rank_eq {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r : ℤ) : Prop

rank_eq G D r holds when r is exactly the rank of D: 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 rank_geq_neg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (k : ℤ) : k < 0 → rank_geq G D k

rank_geq G D k holds vacuously for k < 0, since there are no effective divisors of negative degree.

theorem deg_winnable_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (h_winnable : winnable G D) : deg D ≥ 0

A winnable divisor has nonnegative degree. [Corry-Perkinson], Corollary 1.16

theorem winnable_of_effective {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (h_eff : effective D) : winnable G D

Every effective divisor is winnable (it is already linearly equivalent to itself).

theorem winnable_add_winnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D1 D2 : CFDiv V) (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 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r : ℤ) : r ≥ 0 → rank_geq G D r → r ≤ deg D

If rank_geq G D r holds for some r ≥ 0, then r ≤ deg D. In particular, rank G D ≤ deg D when rank G D ≥ 0.

theorem rank_geq_trans {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r1 r2 : ℤ) : rank_geq G D r1 → r2 ≤ r1 → rank_geq G D r2

rank_geq is downward closed: if rank G D ≥ r1 and r2 ≤ r1, then rank G D ≥ r2.

def lt_of_rank_geq_not {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r1 r2 : ℤ) : rank_geq G D r1 → ¬rank_geq G D r2 → r1 < r2

If rank_geq G D r1 holds but rank_geq G D r2 does not, then r1 < r2.

Equations

• ⋯ = ⋯

theorem rank_eq_neg_one_iff_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : rank_eq G D (-1) ↔ ¬winnable G D

theorem rank_nonneg_iff_winnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : rank_geq G D 0 ↔ winnable G D

rank G D ≥ 0 if and only if D is winnable.

theorem rank_exists_helper {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (m : ℕ) : ¬rank_geq G D ↑m → ∃ r < ↑m, rank_eq G D r

If rank_geq G D m fails for some natural number m, there exists an exact rank r < m.

theorem rank_exists {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : ∃ (r : ℤ), rank_eq G D r

Every divisor has a well-defined rank: there exists r with rank_eq G D r.

theorem rank_unique {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r1 r2 : ℤ) : rank_eq G D r1 → rank_eq G D r2 → r1 = r2

The rank of a divisor is unique: if rank_eq G D r1 and rank_eq G D r2, then r1 = r2.

noncomputable def rank {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : ℤ

The rank function for divisors

Equations

• rank G D = Classical.choose ⋯

theorem rank_geq_iff {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (k : ℤ) : rank_geq G D k ↔ rank G D ≥ k

rank_geq G D k is equivalent to rank G D ≥ k.

theorem rank_eq_iff {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (r : ℤ) : rank_eq G D r ↔ rank G D = r

rank_eq G D r is equivalent to rank G D = r.

theorem winnable_iff_exists_effective {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : winnable G D ↔ ∃ (D' : CFDiv V), effective D' ∧ linear_equiv G D D'

Lemma: If a divisor is winnable, there exists an effective divisor linearly equivalent to it

theorem rank_get_effective {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : ∃ (E : CFDiv V), effective E ∧ deg E = rank G D + 1 ∧ ¬winnable G (D - E)

Lemma: Helper for rank characterization to get effective divisor

theorem rank_neg_one_iff_unwinnable {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : rank G D = -1 ↔ ¬winnable G D

Helpful corollary: rank = -1 exactly when divisor is not winnable

theorem rank_neg_one_of_not_nonneg {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) (h_not_nonneg : ¬rank G D ≥ 0) : rank G D = -1

Lemma: If rank is not non-negative, then it equals -1

theorem rank_geq_neg_one {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) (D : CFDiv V) : rank G D ≥ -1

Lemma: rank ≥ -1

theorem zero_divisor_rank {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : CFGraph V) : rank G 0 = 0

The rank of the zero divisor is zero.