Divisorial gonality as a natural number

The dependency already defines gonalityLeq G k and a noncomputable gonality h_conn : ℤ (ChipFiringWithLean/RiemannRoch.lean). The treewidth/gonality chain wants to compare gonality with treewidth, which is a ℕ, so this module packages the same invariant as an sInf over ℕ and proves the bridges in both directions.

• gonalitySet G : Set ℕ — degrees of effective divisors of rank at least one. Adding effectivity does not change the set of achievable degrees (a divisor of rank ≥ 1 is winnable, and both degree and rank are linear equivalence invariants), but it is the form the van Dobben de Bruyn--Gijswijt argument consumes.
• divisorialGonality G := sInf (gonalitySet G). Nonemptiness of gonalitySet for connected G (gonalitySet_nonempty, via the dependency's gonality_leq_genus_add_one) is what makes the sInf meaningful rather than the sInf ∅ = 0 default; every statement that needs it takes graphConnected G.
• Bridges: BNExists_one_divisorialGonality, divisorialGonality_le_of_BNExists, and gonality_eq_divisorialGonality (the dependency's ℤ-valued gonality is the coercion of this one).

Effective representatives

theorem Utilities.Gonality.exists_effective_of_rank_ge_one {G : CFGraph} {D : CFDiv G} (hD : rank G D ≥ 1) : ∃ (E : CFDiv G), effective E ∧ CFDiv.degree E = CFDiv.degree D ∧ rank G E ≥ 1

A divisor of rank at least one has an effective representative of the same degree and rank.

theorem Utilities.Gonality.one_le_deg_of_rank_ge_one {G : CFGraph} {D : CFDiv G} (hD : rank G D ≥ 1) : 1 ≤ CFDiv.degree D

A divisor of rank at least one has degree at least one.

The gonality set and divisorialGonality

def Utilities.Gonality.gonalitySet (G : CFGraph) : Set ℕ

The degrees of the effective divisors of rank at least one.

Equations

• Utilities.Gonality.gonalitySet G = {d : ℕ | ∃ (D : CFDiv G), effective D ∧ CFDiv.degree D = ↑d ∧ rank G D ≥ 1}

noncomputable def Utilities.Gonality.divisorialGonality (G : CFGraph) : ℕ

The divisorial gonality of G: the least degree of an effective divisor of rank at least one, as a natural number.

Equations

• Utilities.Gonality.divisorialGonality G = sInf (Utilities.Gonality.gonalitySet G)

theorem Utilities.Gonality.mem_gonalitySet {G : CFGraph} {d : ℕ} {D : CFDiv G} (hEff : effective D) (hDeg : CFDiv.degree D = ↑d) (hRank : rank G D ≥ 1) : d ∈ gonalitySet G

Membership in gonalitySet from an explicit witness.

theorem Utilities.Gonality.gonalitySet_nonempty {G : CFGraph} (h_conn : graphConnected G) : (gonalitySet G).Nonempty

On a connected graph there is an effective divisor of rank at least one (of degree genus G + 1), so divisorialGonality is an infimum over a nonempty set.

theorem Utilities.Gonality.divisorialGonality_le {G : CFGraph} {d : ℕ} {D : CFDiv G} (hEff : effective D) (hDeg : CFDiv.degree D = ↑d) (hRank : rank G D ≥ 1) : divisorialGonality G ≤ d

Any effective divisor of rank at least one bounds the gonality.

theorem Utilities.Gonality.exists_divisor_of_divisorialGonality {G : CFGraph} (h_conn : graphConnected G) : ∃ (D : CFDiv G), effective D ∧ CFDiv.degree D = ↑(divisorialGonality G) ∧ rank G D ≥ 1

The gonality is realized by an actual divisor.

theorem Utilities.Gonality.one_le_divisorialGonality {G : CFGraph} (h_conn : graphConnected G) : 1 ≤ divisorialGonality G

The gonality of a connected graph is at least one.

theorem Utilities.Gonality.divisorialGonality_le_genus_add_one {G : CFGraph} (h_conn : graphConnected G) : ↑(divisorialGonality G) ≤ G.genus + 1

divisorialGonality G ≤ genus G + 1 for connected G.

Bridges to BNExists and to the dependency's gonality

theorem Utilities.Gonality.BNExists_one_divisorialGonality {G : CFGraph} (h_conn : graphConnected G) : BNExists G 1 ↑(divisorialGonality G)

The gonality divisor is a rank-one Brill--Noether witness.

theorem Utilities.Gonality.divisorialGonality_le_of_BNExists {G : CFGraph} {d : ℤ} (h : BNExists G 1 d) : ↑(divisorialGonality G) ≤ d

Any rank-one Brill--Noether witness bounds the gonality.

theorem Utilities.Gonality.gonality_leq_divisorialGonality {G : CFGraph} (h_conn : graphConnected G) : gonalityLeq G ↑(divisorialGonality G)

The dependency's predicate gonalityLeq holds at the gonality.

theorem Utilities.Gonality.bddBelow_gonality_leq (G : CFGraph) : BddBelow {k : ℤ | gonalityLeq G k}

The set the dependency takes an sInf over is bounded below by 1.

theorem Utilities.Gonality.gonality_eq_divisorialGonality {G : CFGraph} (h_conn : graphConnected G) : gonality h_conn = ↑(divisorialGonality G)

The two gonalities agree: the dependency's ℤ-valued gonality is the coercion of divisorialGonality.