Orientations of chip-firing graphs

This file defines orientations of chip-firing graphs and establishes their relationship to divisors, configurations, and the Riemann-Roch theorem.

An orientation (CFOrientation G) assigns a direction to each edge of $G$. The key objects are:

• indeg G O v: the in-degree of vertex $v$ under orientation $\mathcal{O}$.
• ordiv G O: the divisor $D(\mathcal{O})$ assigning $\mathrm{indeg}(v) - 1$ to each vertex.
• orientation_to_config G O q: the configuration $c(\mathcal{O})$ for acyclic orientations with unique source $q$.

The main results are:

• Theorem 4.8: There is a bijection between acyclic orientations with unique source $q$ and maximal superstable configurations (orientation_superstable_bijection).
• The divisor of an acyclic orientation is unwinnable (ordiv_unwinnable).
• The canonical divisor $K_G = D(\mathcal{O}) + D(\overline{\mathcal{O}})$ where $\overline{\mathcal{O}}$ is the reverse orientation (divisor_reverse_orientation).
• The degree of the canonical divisor is $2g-2$ (degree_of_canonical_divisor).

See: Corry-Perkinson, Theorem 4.8.

structure CFOrientation (G : CFGraph) : Type u_1

An orientation of $G$ assigns a direction to each edge.

The field directed_edges is a multiset of directed pairs. The count_preserving field ensures that the total flow between $v$ and $w$ equals the edge multiplicity, and no_bidirectional ensures that parallel edges are all directed the same way.

• directed_edges : Multiset (G.V × G.V)

  The multiset of directed edges in the orientation.

• count_preserving (v w : G.V) : num_edges G v w = Multiset.count (v, w) self.directed_edges + Multiset.count (w, v) self.directed_edges

  The total directed flow between two vertices preserves the graph's edge multiplicity.

• no_bidirectional (v w : G.V) : Multiset.count (v, w) self.directed_edges = 0 ∨ Multiset.count (w, v) self.directed_edges = 0

  No edge is directed both ways.

@[reducible, inline]

abbrev flow {G : CFGraph} (O : CFOrientation G) (u v : G.V) : ℕ

The flow from $u$ to $v$ under an orientation $\mathcal{O}$ is the multiplicity of the directed edge $(u,v)$.

Equations

• flow O u v = Multiset.count (u, v) O.directed_edges

def indeg (G : CFGraph) (O : CFOrientation G) (v : G.V) : ℕ

The number of edges directed into a vertex under an orientation.

Equations

• indeg G O v = (Multiset.filter (fun (e : G.V × G.V) => e.2 = v) O.directed_edges).card

def outdeg (G : CFGraph) (O : CFOrientation G) (v : G.V) : ℕ

The number of edges directed out of a vertex under an orientation.

Equations

• outdeg G O v = (Multiset.filter (fun (e : G.V × G.V) => e.1 = v) O.directed_edges).card

def is_source (G : CFGraph) (O : CFOrientation G) (v : G.V) : Prop

A vertex is a source if it has no incoming edges.

Equations

• is_source G O v = (indeg G O v = 0)

def directed_edge (G : CFGraph) (O : CFOrientation G) (u v : G.V) : Prop

The proposition directed_edge G O u v holds when there is a directed edge from $u$ to $v$ in orientation $\mathcal{O}$.

Equations

• directed_edge G O u v = ((u, v) ∈ O.directed_edges)

structure DirectedPath {G : CFGraph} (O : CFOrientation G) : Type u_1

A directed path in a graph under an orientation.

• vertices : List G.V

  The sequence of vertices in the path.

• non_empty : self.vertices.length > 0

  The path is nonempty.

• valid_edges : List.IsChain (directed_edge G O) self.vertices

  Every consecutive pair forms a directed edge.

def non_repeating {G : CFGraph} {O : CFOrientation G} (p : DirectedPath O) : Prop

A directed path is non-repeating if its vertex list has no duplicates.

Equations

• non_repeating p = p.vertices.Nodup

def is_acyclic (G : CFGraph) (O : CFOrientation G) : Prop

An orientation is acyclic if every directed path has no repeated vertices.

Equations

• is_acyclic G O = ∀ (p : DirectedPath O), non_repeating p

def acyclic_with_unique_source (G : CFGraph) (O : CFOrientation G) (q : G.V) : Prop

The proposition acyclic_with_unique_source G O q means that $\mathcal{O}$ is acyclic and every source of $\mathcal{O}$ is equal to $q$.

Equations

• acyclic_with_unique_source G O q = (is_acyclic G O ∧ ∀ (w : G.V), is_source G O w → w = q)

def config_of_source {G : CFGraph} {O : CFOrientation G} {q : G.V} (hO : acyclic_with_unique_source G O q) : Config G q

The configuration associated to an acyclic orientation with unique source $q$ assigns $\mathrm{indeg}(v)-1$ chips to each vertex $v \ne q$, and $0$ at $q$.

Equations

• config_of_source hO = { chips := fun (v : G.V) => if v = q then 0 else ↑(indeg G O v) - 1, q_zero := ⋯, non_negative := ⋯ }

Orientation divisors and configurations

For an orientation $\mathcal{O}$ of $G$, the orientation divisor ordiv G O is $D(\mathcal{O})(v) = \mathrm{indeg}_{\mathcal{O}}(v) - 1$.

For an acyclic orientation $\mathcal{O}$ with unique source $q$, the associated configuration orientation_to_config G O q assigns $\mathrm{indeg}(v) - 1$ chips to each vertex $v \ne q$. An acyclic orientation is uniquely determined by its in-degree sequence (orientation_determined_by_indegrees), and the divisor of an acyclic orientation is always $q$-reduced and unwinnable.

See: Corry-Perkinson, Definition 4.7.

def ordiv (G : CFGraph) (O : CFOrientation G) : CFDiv G

The divisor associated with an orientation assigns $\mathrm{indeg}(v)-1$ to each vertex.

See: Corry-Perkinson, Definition 4.7, part 1; written $D(\mathcal{O})$ there.

Equations

• ordiv G O v = ↑(indeg G O v) - 1

def orqed {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : q_eff_div G q

The orientation divisor ordiv G O bundled as a $q$-effective divisor, using acyclicity to prove $q$-effectivity.

Equations

• orqed O hO = { D := ordiv G O, h_eff := ⋯ }

def orientation_to_config (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) : Config G q

The configuration $c(\mathcal{O})$ associated to an acyclic orientation $\mathcal{O}$.

See: Corry-Perkinson, Definition 4.7 (part 2).

Equations

• orientation_to_config G O q hO = config_of_source hO

theorem config_and_divisor_from_O {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : orientation_to_config G O q hO = toConfig (orqed O hO)

The configuration associated to an orientation agrees with the configuration obtained from its orientation divisor.

theorem orientation_determined_by_indegrees {G : CFGraph} (O O' : CFOrientation G) : is_acyclic G O → is_acyclic G O' → (∀ (v : G.V), indeg G O v = indeg G O' v) → O = O'

An acyclic orientation is uniquely determined by its in-degree sequence.

See: Corry-Perkinson, Lemma 4.3.

theorem degree_ordiv {G : CFGraph} (O : CFOrientation G) : deg (ordiv G O) = genus G - 1

The degree of an orientation divisor equals $g - 1$, where $g$ is the genus of $G$.

theorem config_degree_from_O {G : CFGraph} (O : CFOrientation G) {q : G.V} (hO : acyclic_with_unique_source G O q) : config_degree (orientation_to_config G O q hO) = genus G

The configuration degree of an acyclic orientation with unique source equals the genus.

theorem ordiv_unwinnable (G : CFGraph) (O : CFOrientation G) : is_acyclic G O → ¬winnable G (ordiv G O)

The orientation divisor $D(\mathcal{O})$ of an acyclic orientation $\mathcal{O}$ is not winnable.

See: Corry-Perkinson, Proposition 4.11.

The canonical divisor and reverse orientations

The canonical divisor of $G$ is $K_G(v) = \deg(v) - 2$ for each vertex $v$. The reverse orientation $\overline{\mathcal{O}}$ of an orientation $\mathcal{O}$ is obtained by reversing all edge directions. The key identity is $D(\mathcal{O}) + D(\overline{\mathcal{O}}) = K_G$ (divisor_reverse_orientation).

Combining the handshaking theorem (sum_vertex_degree_eq_twice_card_edges, proved at the end of Basic.lean) with the definition of the genus shows that $\deg(K_G) = 2g - 2$ (degree_of_canonical_divisor).

See: Corry-Perkinson, Definition 5.7.

def canonical_divisor (G : CFGraph) : CFDiv G

The canonical divisor assigns $\deg(v)-2$ to each vertex $v$.

It is independent of orientation and equals $D(\mathcal{O}) + D(\overline{\mathcal{O}})$.

Equations

• canonical_divisor G v = vertex_degree G v - 2

def CFOrientation.reverse (G : CFGraph) (O : CFOrientation G) : CFOrientation G

The reverse orientation $\overline{\mathcal{O}}$ obtained by reversing all edge directions.

See: Corry-Perkinson, Definition 5.7.

Equations

• CFOrientation.reverse G O = { directed_edges := Multiset.map Prod.swap O.directed_edges, count_preserving := ⋯, no_bidirectional := ⋯ }

theorem is_acyclic_reverse_of_is_acyclic (G : CFGraph) (O : CFOrientation G) (h_acyclic : is_acyclic G O) : is_acyclic G (CFOrientation.reverse G O)

The reverse of an acyclic orientation is also acyclic.

theorem divisor_reverse_orientation {G : CFGraph} (O : CFOrientation G) : ordiv G O + ordiv G (CFOrientation.reverse G O) = canonical_divisor G

The orientation divisors of $\mathcal{O}$ and its reverse sum to the canonical divisor: $D(\mathcal{O}) + D(\overline{\mathcal{O}}) = K_G$.

theorem degree_of_canonical_divisor (G : CFGraph) : deg (canonical_divisor G) = 2 * genus G - 2

The degree of the canonical divisor is $2g - 2$, where $g$ is the genus of $G$.

See: Corry-Perkinson, Exercise 5.8.

Orientations from burn lists

Given a complete burn list $L$ for a superstable configuration $c$, the function burn_orientation L h_full constructs an acyclic orientation of $G$ with unique source $q$ (burn_acyclic, burn_unique_source). Acyclicity is proved by showing that position in the burn list gives a strictly decreasing labeling along any directed path (dp_dec).

The key lemma dp_dec formalizes this as a strict chain of natural numbers, and orientation_from_flow constructs a CFOrientation from an explicit flow function.

def multiset_of_count {T : Type u_1} [DecidableEq T] [Fintype T] (f : T → ℕ) : Multiset T

Create a multiset with a given count function. This is a thin wrapper around DFinsupp.toMultiset specialized to a finite type.

Equations

• multiset_of_count f = DFinsupp.toMultiset (DFinsupp.equivFunOnFintype.symm f)

def orientation_from_flow {G : CFGraph} (f : G.V × G.V → ℕ) (h_count_preserving : ∀ (v w : G.V), f (v, w) + f (w, v) = num_edges G v w) (h_no_bidirectional : ∀ (v w : G.V), f (v, w) = 0 ∨ f (w, v) = 0) : CFOrientation G

Constructs a CFOrientation from an explicit flow function, given proofs that it respects edge multiplicities and has no bidirectional edges.

Equations

• orientation_from_flow f h_count_preserving h_no_bidirectional = { directed_edges := multiset_of_count f, count_preserving := ⋯, no_bidirectional := ⋯ }

def burn_orientation {G : CFGraph} {q : G.V} {c : Config G q} (L : burn_list G c) (h_full : ∀ (v : G.V), v ∈ L.list) : CFOrientation G

The orientation constructed from a complete burn list $L$ for a superstable configuration, via burn_flow. This is shown to be acyclic with unique source $q$ by burn_acyclic and burn_unique_source.

Equations

• burn_orientation L h_full = orientation_from_flow (burn_flow L) ⋯ ⋯

The bijection between orientations and maximal superstable configurations

This section establishes Theorem 4.8: there is a bijection between acyclic orientations with unique source $q$ and maximal superstable configurations.

• superstable_dhar: given a superstable configuration $c$, Dhar's algorithm produces an acyclic orientation whose associated configuration dominates $c$.
• orientation_config_maximal: Every acyclic orientation with unique source $q$ gives a maximal superstable configuration.
• maximal_superstable_orientation: Every maximal superstable configuration arises from some acyclic orientation.
• orientation_superstable_bijection: The full bijection statement.

See: Corry-Perkinson, Theorem 4.8.

theorem superstable_dhar {G : CFGraph} {q : G.V} {c : Config G q} (h_ss : superstable G q c) : ∃ (O : CFOrientation G) (hO : acyclic_with_unique_source G O q), c ≤ orientation_to_config G O q hO

Dhar's burning algorithm produces, from a superstable configuration, an orientation whose associated configuration dominates it.

theorem orientation_config_maximal (G : CFGraph) (O : CFOrientation G) (q : G.V) (hO : acyclic_with_unique_source G O q) : maximal_superstable G (orientation_to_config G O q hO)

The configuration associated to an acyclic orientation with unique source is maximal superstable.

See: Corry-Perkinson, Theorem 4.8, part 1 ($c(\mathcal{O})$ is maximal superstable).

theorem maximal_superstable_exists (G : CFGraph) (q : G.V) (c : Config G q) (h_super : superstable G q c) : ∃ (c' : Config G q), maximal_superstable G c' ∧ c ≤ c'

Every superstable configuration extends to a maximal superstable configuration.

theorem maximal_superstable_orientation (G : CFGraph) (q : G.V) (c : Config G q) (h_max : maximal_superstable G c) : ∃ (O : CFOrientation G) (hO : acyclic_with_unique_source G O q), orientation_to_config G O q hO = c

Every maximal superstable configuration comes from an acyclic orientation.

See: Corry-Perkinson, Theorem 4.8, part 2 (surjectivity).

theorem orientation_superstable_bijection (G : CFGraph) (q : G.V) : let α := { O : CFOrientation G // acyclic_with_unique_source G O q }; let β := { c : Config G q // maximal_superstable G c }; let f_raw := fun (O_sub : α) => orientation_to_config G (↑O_sub) q ⋯; have f := fun (O_sub : α) => ⟨f_raw O_sub, ⋯⟩; Function.Bijective f

The bijection between acyclic orientations with unique source $q$ and maximal superstable configurations.

See: Corry-Perkinson, Theorem 4.8, part 3 (bijection).