Adding an edge to a chip-firing graph

This file develops the graph-theoretic infrastructure for genus induction by adding a single edge. The construction keeps the vertex type definitionally unchanged, so divisors and firing scripts on the old and new graphs are the same functions.

@[reducible, inline]

abbrev Utilities.addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : CFGraph

Add one edge between two distinct existing vertices.

Equations

• Utilities.addEdge H x y hxy = { V := H.V, instDecidableEq := H.instDecidableEq, instFintype := H.instFintype, instNonempty := ⋯, edges := (x, y) ::ₘ H.edges, loopless := ⋯ }

@[simp]

theorem Utilities.addEdge_edges (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : (addEdge H x y hxy).edges = (x, y) ::ₘ H.edges

@[simp]

theorem Utilities.num_edges_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (v w : H.V) : numEdges (addEdge H x y hxy) v w = numEdges H v w + if v = x ∧ w = y ∨ v = y ∧ w = x then 1 else 0

theorem Utilities.num_edges_le_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (v w : H.V) : numEdges H v w ≤ numEdges (addEdge H x y hxy) v w

@[simp]

theorem Utilities.deg_on_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (D : H.V → ℤ) : CFDiv.degree D = CFDiv.degree D

A divisor has the same degree when regarded on the graph with the added edge, since the vertex type and its finite structure are unchanged.

theorem Utilities.num_edges_addEdge_endpoints (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : numEdges (addEdge H x y hxy) x y = numEdges H x y + 1

theorem Utilities.num_edges_addEdge_of_not_endpoints (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (v w : H.V) (hvw : ¬(v = x ∧ w = y ∨ v = y ∧ w = x)) : numEdges (addEdge H x y hxy) v w = numEdges H v w

@[simp]

theorem Utilities.genus_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : (addEdge H x y hxy).genus = H.genus + 1

theorem Utilities.graph_connected_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (hH : graphConnected H) : graphConnected (addEdge H x y hxy)

@[simp]

theorem Utilities.vertex_degree_addEdge_left (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : vertexDegree (addEdge H x y hxy) x = vertexDegree H x + 1

@[simp]

theorem Utilities.vertex_degree_addEdge_right (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : vertexDegree (addEdge H x y hxy) y = vertexDegree H y + 1

@[simp]

theorem Utilities.vertex_degree_addEdge_of_ne (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (v : H.V) (hvx : v ≠ x) (hvy : v ≠ y) : vertexDegree (addEdge H x y hxy) v = vertexDegree H v

def Utilities.seamDivisor {H : CFGraph} (x y : H.V) : CFDiv H

The degree-zero divisor supported with opposite signs at the new edge's endpoints.

Equations

• Utilities.seamDivisor x y = oneChip x - oneChip y

@[simp]

theorem Utilities.deg_seamDivisor {H : CFGraph} (x y : H.V) : CFDiv.degree (seamDivisor x y) = 0

theorem Utilities.deg_add_zsmul_seamDivisor {H : CFGraph} (D : CFDiv H) (x y : H.V) (n : ℤ) : CFDiv.degree (D + n • seamDivisor x y) = CFDiv.degree D

theorem Utilities.prin_addEdge_apply_left (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (σ : firingScript H) : (prin (addEdge H x y hxy)) σ x = (prin H) σ x + (σ y - σ x)

theorem Utilities.prin_addEdge_apply_right (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (σ : firingScript H) : (prin (addEdge H x y hxy)) σ y = (prin H) σ y + (σ x - σ y)

theorem Utilities.prin_addEdge_apply_of_ne (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (σ : firingScript H) (v : H.V) (hvx : v ≠ x) (hvy : v ≠ y) : (prin (addEdge H x y hxy)) σ v = (prin H) σ v

theorem Utilities.prin_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (σ : firingScript H) : (prin H) σ = fun (v : H.V) => (prin (addEdge H x y hxy)) σ v + (σ x - σ y) * seamDivisor x y v

Adding an edge changes the principal divisor by a rank-one term.

The sign reflects the convention in ChipFiringWithLean: prin is the negative of the usual graph Laplacian applied to the firing script.

theorem Utilities.linear_equiv_phase_transfer (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (D E : CFDiv H) (hDE : linearEquiv H D E) : ∃ (n : ℤ), linearEquiv (addEdge H x y hxy) (D + n • seamDivisor x y) E

Linear equivalence on the old graph transfers to linear equivalence on the new graph after translating by an integral multiple of the seam divisor.

theorem Utilities.phase_represented_by_old_linear_class (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (D : CFDiv H) (n : ℤ) : ∃ (E : CFDiv H), linearEquiv H D E ∧ linearEquiv (addEdge H x y hxy) (D + n • seamDivisor x y) E

Conversely, every integral seam phase is represented on the enlarged graph by a divisor linearly equivalent to D on the old graph.

theorem Utilities.old_linear_class_iff_seam_phase_orbit (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (D F : CFDiv H) : (∃ (E : CFDiv H), linearEquiv H D E ∧ linearEquiv (addEdge H x y hxy) E F) ↔ ∃ (n : ℤ), linearEquiv (addEdge H x y hxy) (D + n • seamDivisor x y) F

Exact orbit description: the classes on the enlarged graph represented by the old linear class of D are precisely the integral seam phases of D.

theorem Utilities.winnable_phase_transfer (H : CFGraph) (x y : H.V) (hxy : x ≠ y) (D : CFDiv H) (hD : winnable H D) : ∃ (n : ℤ), winnable (addEdge H x y hxy) (D + n • seamDivisor x y)

A winnable divisor on the old graph has a winnable phase after the edge is added. This is edge normalization in rank zero, without a BN hypothesis.

theorem Utilities.canonical_divisor_addEdge (H : CFGraph) (x y : H.V) (hxy : x ≠ y) : canonicalDivisor (addEdge H x y hxy) = fun (v : H.V) => canonicalDivisor H v + oneChip x v + oneChip y v

Adding the edge increases the canonical divisor by one chip at each endpoint. The pointwise RHS makes the definitional identification of vertex types explicit.