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 ChipFiring.winnable_equiv_winnable (G : CFGraph) (D1 D2 : CFDiv G) : winnable G D1 → linearEquiv G D1 D2 → winnable G D2

Winnability is preserved under linear equivalence.

def ChipFiring.maximalUnwinnable (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

• ChipFiring.maximalUnwinnable G D = (¬ChipFiring.winnable G D ∧ ∀ (v : G.V), ChipFiring.winnable G (D + ChipFiring.oneChip v))

theorem ChipFiring.maximal_unwinnable_preserved (G : CFGraph) (D1 D2 : CFDiv G) : maximalUnwinnable G D1 → linearEquiv G D1 D2 → maximalUnwinnable G D2

Being maximal unwinnable is preserved under linear equivalence.

def ChipFiring.effOfDegree (G : CFGraph) (k : ℤ) : Set (CFDiv G)

The set of effective divisors of degree $k$.

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

Equations

• ChipFiring.effOfDegree G k = {E : ChipFiring.CFDiv G | ChipFiring.effective E ∧ ChipFiring.deg E = k}

def ChipFiring.rankGeq (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

• ChipFiring.rankGeq G D k = ∀ E ∈ ChipFiring.effOfDegree G k, ChipFiring.winnable G (D - E)

def ChipFiring.rankEq (G : CFGraph) (D : CFDiv G) (r : ℤ) : Prop

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

Equations

• ChipFiring.rankEq G D r = (ChipFiring.rankGeq G D r ∧ ¬ChipFiring.rankGeq G D (r + 1))

theorem ChipFiring.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 ChipFiring.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 ChipFiring.rank_le_degree (G : CFGraph) (D : CFDiv G) (r : ℤ) : r ≥ 0 → rankGeq 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 ChipFiring.lt_of_rank_geq_not (G : CFGraph) (D : CFDiv G) (r1 r2 : ℤ) : rankGeq G D r1 → ¬rankGeq 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 ChipFiring.rank_nonneg_iff_winnable (G : CFGraph) (D : CFDiv G) : rankGeq G D 0 ↔ winnable G D

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

theorem ChipFiring.rank_exists (G : CFGraph) (D : CFDiv G) : ∃ (r : ℤ), rankEq G D r

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

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

The rank function for divisors.

Equations

• ChipFiring.rank G D = Classical.choose ⋯

theorem ChipFiring.rank_geq_iff (G : CFGraph) (D : CFDiv G) (k : ℤ) : rankGeq G D k ↔ rank G D ≥ k

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

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

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

theorem ChipFiring.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 ChipFiring.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 ChipFiring.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 ChipFiring.rank_geq_neg_one (G : CFGraph) (D : CFDiv G) : rank G D ≥ -1

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

theorem ChipFiring.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 ChipFiring.zero_divisor_rank (G : CFGraph) : rank G 0 = 0

The rank of the zero divisor is zero.

theorem ChipFiring.one_le_apply_of_q_reduced_of_rank_geq_one {G : CFGraph} {q : G.V} {D : CFDiv G} (hred : qReduced G q D) (hrank : rank G D ≥ 1) : 1 ≤ D q