Support complexes of rank-zero divisors

The paper calls the vertices reachable by one chip from a divisor its support complex. Here it is expressed directly with the existing rank API. The main criterion is Lemma 3.1(2) of the paper, stated without choosing an effective representative.

def Bananas.rankSupport (G : CFGraph) (D : CFDiv G) : Set G.V

The support complex of D: vertices whose one-chip deletion is still winnable (equivalently, has nonnegative rank).

Equations

• Bananas.rankSupport G D = {x : G.V | 0 ≤ rank G (D - oneChip x)}

@[simp]

theorem Bananas.mem_rankSupport_iff (G : CFGraph) (D : CFDiv G) (x : G.V) : x ∈ rankSupport G D ↔ 0 ≤ rank G (D - oneChip x)

theorem Bananas.rank_sub_one_chip_le_rank (G : CFGraph) (D : CFDiv G) (q : G.V) : rank G (D - oneChip q) ≤ rank G D

Removing one chip cannot increase rank.

theorem Bananas.mem_rankSupport_iff_rank_eq_zero_of_rank_zero (G : CFGraph) (D : CFDiv G) (hD : rank G D = 0) (x : G.V) : x ∈ rankSupport G D ↔ rank G (D - oneChip x) = 0

For a rank-zero divisor, its support is precisely the set of vertices whose deletion has rank zero.

theorem Bananas.rankDelta_neg_iff_rankSupport_pattern (M : TwiceMarked) (D : CFDiv M.graph) (hD : rank M.graph D = 0) : rankDelta M D < 0 ↔ (M.v ∈ rankSupport M.graph D ∧ M.v ∉ rankSupport M.graph (D - oneChip M.u)) ∧ M.u ∈ rankSupport M.graph D ∧ M.u ∉ rankSupport M.graph (D - oneChip M.v)

Rank-zero support criterion (paper Lemma 3.1(2)). At rank zero a negative marked second difference is exactly the assertion that each mark is reachable from D, but not after deleting the other mark.