Degree-two divisors on a connected genus-two graph

These coordinate-free Riemann--Roch facts are the algebraic core needed for the theta transmission-characterization proposition in Section 4. Keeping them at an abstract graph prevents later theta proofs from unfolding concrete subdivision vertices during divisor algebra.

theorem Bananas.rank_le_zero_of_degree_zero (G : CFGraph) (X : CFDiv G) (hDegree : CFDiv.degree X = 0) : rank G X ≤ 0

A degree-zero divisor has rank at most zero.

theorem Bananas.rank_le_one_of_degree_two_genus_two {G : CFGraph} (hconn : _root_.graphConnected G) (hgenus : G.genus = 2) (X : CFDiv G) (hDegree : CFDiv.degree X = 2) : rank G X ≤ 1

On a connected genus-two graph, a degree-two divisor has rank at most one.

theorem Bananas.rank_canonical_eq_one_of_genus_two {G : CFGraph} (hconn : _root_.graphConnected G) (hgenus : G.genus = 2) : rank G (canonicalDivisor G) = 1

The canonical divisor has rank one on every connected genus-two graph.

theorem Bananas.linearEquiv_canonical_of_rank_eq_one_degree_two_genus_two {G : CFGraph} (hconn : _root_.graphConnected G) (hgenus : G.genus = 2) (X : CFDiv G) (hDegree : CFDiv.degree X = 2) (hRank : rank G X = 1) : linearEquiv G X (canonicalDivisor G)

A rank-one degree-two divisor is the canonical class.

theorem Bananas.rank_eq_one_iff_linearEquiv_canonical_of_degree_two_genus_two {G : CFGraph} (hconn : _root_.graphConnected G) (hgenus : G.genus = 2) (X : CFDiv G) (hDegree : CFDiv.degree X = 2) : rank G X = 1 ↔ linearEquiv G X (canonicalDivisor G)

On a connected genus-two graph, a degree-two divisor has rank one exactly when it is linearly equivalent to the canonical divisor.