Transport of divisorial gonality, and gonality over regular subdivisions

This module supplies three ingredients for the tricycle formalization:

1. divisorialGonality_of_laplacianEquiv — divisorial gonality is an invariant of the Laplacian, so every presentation of a graph computes the same number.
2. rank_ge_of_add_effective and le_divisorialGonality_of_forall — the two little lemmas that turn "no positive-rank divisor of degree exactly d, for each d < k" into the bound k ≤ divisorialGonality.
3. Spec.scale, Spec.regularSubdivisionGonality, and their CFGraph-level counterparts regularSubdivision / regularSubdivisionGonality — the invariant min_{k ≥ 1} dgon(σ_k(G)).

What the name regularSubdivisionGonality does and does not claim

Van Dobben de Bruyn–Smit–van der Wegen's Theorem 1.5 identifies min_{k ≥ 1} dgon(σ_k(G)) with the divisorial gonality of the metric graph Γ(G, 𝟙). That theorem needs metric graphs, piecewise-linear rational functions, Luo's Theorems 1.6 and 1.10, and a rational-LP lemma; none of that is formalized here, and none of it is needed for the tricycle gap. So the invariant is not called metricGonality. The identification with the metric gonality is external and unformalized.

It is also not stableGonality, which is taken and means something strictly smaller: Bodlaender–van der Wegen–van der Zanden (arXiv:1808.06921) define stable divisorial gonality as the minimum of dgon over all subdivisions, with independent per-edge subdivision counts, and Cornelissen–Kato–Kool's stable gonality additionally allows adding leaves. A subdivision with unequal per-edge counts is the unit model of a different metric graph Γ(G, ℓ), so sdgon(G) ≤ regularSubdivisionGonality G, possibly strictly.

Adding an effective divisor cannot lower the rank below one

theorem Utilities.Gonality.rank_ge_of_add_effective {G : CFGraph} {D E : CFDiv G} (hE : effective E) (hD : rank G D ≥ 1) : rank G (D + E) ≥ 1

Adding an effective divisor preserves positive rank. This is what upgrades "no positive-rank divisor of degree exactly d" to a gonality bound without re-running the smaller degrees.

Lower bounds on divisorialGonality

theorem Utilities.Gonality.le_divisorialGonality_of_forall {G : CFGraph} (h_conn : graphConnected G) {k : ℕ} (h : ∀ (D : CFDiv G), effective D → rank G D ≥ 1 → ↑k ≤ CFDiv.degree D) : k ≤ divisorialGonality G

Bounding the gonality from below is exactly bounding the degree of every positive-rank effective divisor from below.

theorem Utilities.Gonality.le_divisorialGonality_of_no_small {G : CFGraph} (h_conn : graphConnected G) {k : ℕ} (h : ∀ (D : CFDiv G), effective D → CFDiv.degree D = ↑k - 1 → ¬rank G D ≥ 1) : k ≤ divisorialGonality G

The form the tricycle lower bounds are actually proved in: no positive-rank effective divisor of degree exactly d for any d < k. rank_ge_of_add_effective is what lets the smaller degrees be skipped.

Divisorial gonality is a Laplacian invariant

theorem Utilities.Gonality.gonalitySet_eq_of_laplacianEquiv {G : CFGraph} {H : CFGraph} (equivalence : Certificate.LaplacianEquiv G H) : gonalitySet G = gonalitySet H

theorem Utilities.Gonality.divisorialGonality_of_laplacianEquiv {G : CFGraph} {H : CFGraph} (equivalence : Certificate.LaplacianEquiv G H) : divisorialGonality G = divisorialGonality H

Divisorial gonality is an invariant of the Laplacian. Every presentation of the same graph computes the same number.

Regular subdivisions of a Spec

def Utilities.Certificate.SubdivisionGraph.Spec.scale {n p : ℕ} (spec : Spec n p) (k : ℕ) (hk : 0 < k) : Spec n p

σ_k of a subdivision specification: multiply every slot length by k.

Equations

• spec.scale k hk = { core := spec.core, length := fun (edge : Fin p) => k * spec.length edge, core_nonempty := ⋯, core_loopless := ⋯, length_pos := ⋯ }

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.scale_length {n p : ℕ} (spec : Spec n p) (k : ℕ) (hk : 0 < k) (edge : Fin p) : (spec.scale k hk).length edge = k * spec.length edge

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.scale_core {n p : ℕ} (spec : Spec n p) (k : ℕ) (hk : 0 < k) : (spec.scale k hk).core = spec.core

def Utilities.Certificate.SubdivisionGraph.Spec.scaleOneRelabeling {n p : ℕ} (spec : Spec n p) : (spec.scale 1 Nat.one_pos).Relabeling spec

Scaling by one changes nothing (up to the relabeling that fixes everything and only adjusts 1 * L to L).

Equations

• spec.scaleOneRelabeling = { coreEquiv := Equiv.refl (Fin n), slotEquiv := Equiv.refl (Fin p), reversed := fun (x : Fin p) => false, length_eq := ⋯, tail_eq := ⋯, head_eq := ⋯ }

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.regularSubdivisionGonality {n p : ℕ} (spec : Spec n p) : ℕ

The regular-subdivision gonality of a subdivision-presented graph: min_{k ≥ 1} dgon(σ_k), where σ_k multiplies every slot length by k.

See the module docstring for why this is neither metricGonality nor stableGonality.

Equations

• spec.regularSubdivisionGonality = sInf {d : ℕ | ∃ (k : ℕ) (hk : 0 < k), Utilities.Gonality.divisorialGonality (spec.scale k hk).graph = d}

theorem Utilities.Certificate.SubdivisionGraph.Spec.regularSubdivisionGonalitySet_nonempty {n p : ℕ} (spec : Spec n p) : {d : ℕ | ∃ (k : ℕ) (hk : 0 < k), Gonality.divisorialGonality (spec.scale k hk).graph = d}.Nonempty

theorem Utilities.Certificate.SubdivisionGraph.Spec.regularSubdivisionGonality_le {n p : ℕ} (spec : Spec n p) {k : ℕ} (hk : 0 < k) {d : ℕ} (h : Gonality.divisorialGonality (spec.scale k hk).graph = d) : spec.regularSubdivisionGonality ≤ d

The gonality of some σ_k bounds the invariant from above.

theorem Utilities.Certificate.SubdivisionGraph.Spec.le_regularSubdivisionGonality {n p : ℕ} (spec : Spec n p) {d : ℕ} (h : ∀ (k : ℕ) (hk : 0 < k), d ≤ Gonality.divisorialGonality (spec.scale k hk).graph) : d ≤ spec.regularSubdivisionGonality

A uniform lower bound over all k bounds the invariant from below.

theorem Utilities.Certificate.SubdivisionGraph.Spec.regularSubdivisionGonality_le_divisorialGonality {n p : ℕ} (spec : Spec n p) : spec.regularSubdivisionGonality ≤ Gonality.divisorialGonality spec.graph

The invariant never exceeds the divisorial gonality itself (k = 1).

Regular subdivisions of an arbitrary CFGraph

noncomputable def Utilities.Gonality.regularSubdivision (G : CFGraph) (k : ℕ) (hk : 0 < k) : CFGraph

σ_k(G) for an arbitrary finite loopless multigraph, built on the occurrence-safe unit subdivision presentation of G.

Equations

• Utilities.Gonality.regularSubdivision G k hk = ((Utilities.Certificate.UnitSubdivisionPresentation.spec G).scale k hk).graph

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

min_{k ≥ 1} dgon(σ_k(G)) for an arbitrary finite loopless multigraph.

Equations

• Utilities.Gonality.regularSubdivisionGonality G = (Utilities.Certificate.UnitSubdivisionPresentation.spec G).regularSubdivisionGonality

theorem Utilities.Gonality.regularSubdivisionGonality_le_divisorialGonality (G : CFGraph) : regularSubdivisionGonality G ≤ divisorialGonality G