Highlights of the Utilities library

A public interface, in one file. Every main theorem of this library is restated below as an example whose type is written out in full and whose proof is the real theorem. Nothing here is new mathematics — there is not a single new definition or theorem in this file.

The point is twofold.

• For a reader. The complete statement of each headline result is visible here, with all of its binders and hypotheses, without navigating ninety modules.
• For the build. Because each example is checked by the kernel against the real declaration, a refactor that silently changes a statement — weakens a hypothesis, strengthens a conclusion, renames a definition — breaks this file loudly, in seconds. That is the whole reason the statements are spelled out rather than abbreviated.

Utilities is infrastructure: it holds only what more than one downstream programme uses. Its headline content is accordingly an API rather than a single named theorem — the divisorial gonality interface (attainment, the agreement of the two gonality conventions, the nested legal chain to a q-reduced form) and the transport of Brill–Noether data along a relabelling.

The named theorems that used to head this file now head their own libraries, because each is an application of this infrastructure rather than a piece of it:

• treewidth ≤ gonality (van Dobben de Bruyn–Gijswijt) — TreewidthGonality/, restated in TreewidthGonality/Highlights.lean;
• the discrete/metric gonality gap (van Dobben de Bruyn–Smit–van der Wegen) — Tricycle/, restated in Tricycle/Highlights.lean.

The key definitions

Re-exported here so that the statements below read without qualification.

def Utilities.Highlights.underlyingSimpleGraph (G : CFGraph) : SimpleGraph G.V

The simple graph underlying a chip-firing multigraph: v and w are adjacent when numEdges G v w > 0. "The treewidth of a multigraph" means the treewidth of this graph — parallel edges do not change it. (Utilities/Foundations/UnderlyingSimpleGraph.lean)

Equations

• Utilities.Highlights.underlyingSimpleGraph = Utilities.underlyingSimpleGraph

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

The degrees of the effective divisors of rank at least one. (Utilities/Gonality/DivisorialGonality.lean)

Equations

• Utilities.Highlights.gonalitySet = Utilities.Gonality.gonalitySet

def Utilities.Highlights.divisorialGonality (G : CFGraph) : ℕ

Divisorial gonality: the least degree of an effective divisor of rank at least one, as a natural number. An Nat.sInf, so it is attained whenever gonalitySet is nonempty — which it is on a connected graph. (Utilities/Gonality/DivisorialGonality.lean)

Equations

• Utilities.Highlights.divisorialGonality = Utilities.Gonality.divisorialGonality

def Utilities.Highlights.fireChain (G : CFGraph) (D : CFDiv G) (U : ℕ → Finset G.V) : ℕ → CFDiv G

Iterated set firing: fireChain G D U i fires U 0, …, U (i-1) in turn. (Utilities/Gonality/LegalFiring.lean)

Equations

• Utilities.Highlights.fireChain = Utilities.Gonality.fireChain

def Utilities.Highlights.CFGraphIso (G : CFGraph) (H : CFGraph) : Type (max u v)

An isomorphism of chip-firing graphs: a vertex bijection preserving every edge multiplicity. (Utilities/Iso/GraphIso.lean)

Equations

• Utilities.Highlights.CFGraphIso = Utilities.CFGraphIso

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

There is a divisor of degree d and rank at least r on G. (Utilities/Foundations/Parameters.lean)

Equations

• Utilities.Highlights.BNExists = Utilities.BNExists

def Utilities.Highlights.fossil (G : CFGraph) : CFGraph

The fossil: the library's short name for the degree-one Abel--Jacobi image, equivalently the 2-edge-connectivization of a connected graph. (Utilities/Iso/Fossil.lean)

Equations

• Utilities.Highlights.fossil = Utilities.fossil

The gonality API

This is what every downstream gonality argument in the repository runs on.

The Abel--Jacobi image / fossil

Transport along a relabelling