Riemann--Roch duality for Brill--Noether existence

Graph Riemann--Roch identifies the rank condition for a divisor D with the dual rank condition for K_G - D. This module records both the pointwise rank equivalence and the induced symmetry of BNExists.

theorem Utilities.rank_ge_iff_dual_rank_ge {G : CFGraph} (hG : graphConnected G) (D : CFDiv G) (r : ℤ) : rank G D ≥ r ↔ rank G (canonicalDivisor G - D) ≥ dualRank G r (CFDiv.degree D)

Riemann--Roch converts a rank lower bound into the complementary one.

theorem Utilities.rectangleWidth_dual (G : CFGraph) (r d : ℤ) : rectangleWidth G (dualRank G r d) (dualDegree G d) = r + 1

Duality transposes the Brill--Noether rectangle.

theorem Utilities.bnNumber_dual (G : CFGraph) (r d : ℤ) : bnNumber G (dualRank G r d) (dualDegree G d) = bnNumber G r d

The dual parameter operation preserves the Brill--Noether number.

@[simp]

theorem Utilities.dualDegree_dualDegree (G : CFGraph) (d : ℤ) : dualDegree G (dualDegree G d) = d

Taking the dual degree twice recovers the original degree.

@[simp]

theorem Utilities.dualRank_dual (G : CFGraph) (r d : ℤ) : dualRank G (dualRank G r d) (dualDegree G d) = r

Taking dual parameters twice recovers the original rank.

theorem Utilities.BNExists_dual_iff {G : CFGraph} (hG : graphConnected G) (r d : ℤ) : BNExists G r d ↔ BNExists G (dualRank G r d) (dualDegree G d)

Brill--Noether existence is invariant under Riemann--Roch duality.