Brill--Noether parameters

This module fixes the integer parameter conventions used throughout the library. For a graph of genus g, the Brill--Noether rectangle associated to rank r and degree d has height r + 1 and width g - d + r.

The existence predicate deliberately includes the degree equality. This makes duality and later arithmetic reductions insensitive to the particular divisor chosen as a witness.

def Utilities.rectangleWidth (G : CFGraph) (r d : ℤ) : ℤ

The width g - d + r of the Brill--Noether rectangle.

Equations

• Utilities.rectangleWidth G r d = G.genus - d + r

def Utilities.bnNumber (G : CFGraph) (r d : ℤ) : ℤ

The Brill--Noether number g - (r + 1) * (g - d + r).

Equations

• Utilities.bnNumber G r d = G.genus - (r + 1) * Utilities.rectangleWidth G r d

def Utilities.BNExists (G : CFGraph) (r d : ℤ) : Prop

There is a divisor of degree d and rank at least r on G.

Equations

• Utilities.BNExists G r d = ∃ (D : CFDiv G), CFDiv.degree D = d ∧ rank G D ≥ r

def Utilities.dualDegree (G : CFGraph) (d : ℤ) : ℤ

The degree complementary to d with respect to the canonical divisor.

Equations

• Utilities.dualDegree G d = 2 * G.genus - 2 - d

def Utilities.dualRank (G : CFGraph) (r d : ℤ) : ℤ

The dual rank g - d + r - 1.

Equations

• Utilities.dualRank G r d = Utilities.rectangleWidth G r d - 1