Removing genus-zero factors from a vertex wedge

A connected genus-zero factor has the rank profile of a point: the rank of a divisor is its degree when that degree is nonnegative, and is -1 otherwise. Substitution in the exact vertex-wedge rank formula therefore absorbs the whole factor into the coefficient of the gluing vertex on the other factor.

This is the zero-genus reduction needed at the endpoints of the balancing argument in Corollary 6.16(2) of the banana-graph paper.

theorem Bananas.rank_eq_degree_of_connected_genus_zero (H : CFGraph) (hConnected : graphConnected H) (hGenus : H.genus = 0) (E : CFDiv H) (hDegree : 0 ≤ CFDiv.degree E) : rank H E = CFDiv.degree E

On a connected genus-zero graph, every divisor of nonnegative degree has rank equal to its degree.

theorem Bananas.rank_eq_degree_or_neg_one_of_connected_genus_zero (H : CFGraph) (hConnected : graphConnected H) (hGenus : H.genus = 0) (E : CFDiv H) : rank H E = if CFDiv.degree E < 0 then -1 else CFDiv.degree E

Complete rank formula on a connected genus-zero graph.

theorem Bananas.rank_vertexWedge_genus_zero_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hConnected : graphConnected H) (hGenus : H.genus = 0) (D : CFDiv G) (E : CFDiv H) : rank (Utilities.vertexWedge G H x y) (Utilities.wedgeAddDivisor G H x y D E) = rank G (D + CFDiv.degree E • oneChip x)

A connected genus-zero factor in a vertex wedge can be absorbed into the gluing coefficient on the other factor. This is an exact rank identity for arbitrary divisors, not merely a Brill--Noether implication.

theorem Bananas.brillNoetherGeneral_vertexWedge_genus_zero_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hConnected : graphConnected H) (hGenus : H.genus = 0) (hGeneral : BrillNoetherGeneral G) : BrillNoetherGeneral (Utilities.vertexWedge G H x y)

Wedging on a connected genus-zero right factor preserves Brill--Noether generality.