Wedges of chip-firing graphs

vertexWedge G H x y is the graph obtained by identifying the selected vertices x : G.V and y : H.V. We represent the identified vertex by Sum.inl x; the other vertices of H are stored in the right summand.

The point of this concrete presentation is that it has literal zero-extension maps for divisors and firing scripts. Later vertex-gluing arguments can use these maps without choosing a quotient representative.

def Utilities.wedgeRightVertex (G : CFGraph) (H : CFGraph) (x : G.V) (y a✝ : H.V) : G.V ⊕ { b : H.V // b ≠ y }

Map the vertices of the right factor into a wedge, sending its marked vertex to the marked vertex on the left.

Equations

• Utilities.wedgeRightVertex G H x y b = if h : b = y then Sum.inl x else Sum.inr ⟨b, h⟩

@[simp]

theorem Utilities.wedgeRightVertex_marked (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : wedgeRightVertex G H x y y = Sum.inl x

@[simp]

theorem Utilities.wedgeRightVertex_unmarked (G : CFGraph) (H : CFGraph) (x : G.V) (y b : H.V) (hb : b ≠ y) : wedgeRightVertex G H x y b = Sum.inr ⟨b, hb⟩

theorem Utilities.wedgeRightVertex_eq_left_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y b : H.V) (a : G.V) : wedgeRightVertex G H x y b = Sum.inl a ↔ b = y ∧ a = x

The only right-factor vertex represented by a left vertex of the wedge is the marked vertex.

@[reducible, inline]

abbrev Utilities.vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFGraph

Identifying x and y in the disjoint union of G and H.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Utilities.vertexWedge_edges (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : (vertexWedge G H x y).edges = Multiset.map (fun (e : G.V × G.V) => (Sum.inl e.1, Sum.inl e.2)) G.edges + Multiset.map (fun (e : H.V × H.V) => (wedgeRightVertex G H x y e.1, wedgeRightVertex G H x y e.2)) H.edges

def Utilities.wedgeLeftVertex (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : G.V → (vertexWedge G H x y).V

The left factor is included literally in the wedge.

Equations

• Utilities.wedgeLeftVertex G H x y = Sum.inl

@[simp]

theorem Utilities.wedgeLeftVertex_apply (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) : wedgeLeftVertex G H x y a = Sum.inl a

def Utilities.wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : CFDiv (vertexWedge G H x y)

A divisor on the wedge obtained by adding a left divisor and a right divisor, with the right marked chip placed at the common vertex.

Equations

• Utilities.wedgeAddDivisor G H x y D E = Sum.elim (fun (a : G.V) => D a + if a = x then E y else 0) fun (b : { b : H.V // b ≠ y }) => E ↑b

def Utilities.wedgeLiftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : CFDiv (vertexWedge G H x y)

Extend a left divisor by zero away from the common vertex.

Equations

• Utilities.wedgeLiftLeftDivisor G H x y D = Utilities.wedgeAddDivisor G H x y D 0

def Utilities.wedgeLiftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (E : CFDiv H) : CFDiv (vertexWedge G H x y)

Extend a right divisor by zero away from the common vertex, placing its marked coefficient at the common vertex.

Equations

• Utilities.wedgeLiftRightDivisor G H x y E = Utilities.wedgeAddDivisor G H x y 0 E

@[simp]

theorem Utilities.wedgeLiftLeftDivisor_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (a : G.V) : wedgeLiftLeftDivisor G H x y D (Sum.inl a) = D a

@[simp]

theorem Utilities.wedgeLiftLeftDivisor_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (b : { b : H.V // b ≠ y }) : wedgeLiftLeftDivisor G H x y D (Sum.inr b) = 0

@[simp]

theorem Utilities.wedgeLiftRightDivisor_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (E : CFDiv H) (a : G.V) : wedgeLiftRightDivisor G H x y E (Sum.inl a) = if a = x then E y else 0

@[simp]

theorem Utilities.wedgeLiftRightDivisor_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (E : CFDiv H) (b : { b : H.V // b ≠ y }) : wedgeLiftRightDivisor G H x y E (Sum.inr b) = E ↑b

@[simp]

theorem Utilities.wedgeAddDivisor_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (a : G.V) : wedgeAddDivisor G H x y D E (Sum.inl a) = D a + if a = x then E y else 0

@[simp]

theorem Utilities.wedgeAddDivisor_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (b : { b : H.V // b ≠ y }) : wedgeAddDivisor G H x y D E (Sum.inr b) = E ↑b

theorem Utilities.sum_unmarked_add_marked (H : CFGraph) (y : H.V) (f : H.V → ℤ) : ∑ b : { b : H.V // b ≠ y }, f ↑b + f y = ∑ b : H.V, f b

Splitting a finite sum into the marked vertex and its complement.

theorem Utilities.sum_unmarked_eq_sum_of_marked_zero (H : CFGraph) (y : H.V) (f : H.V → ℤ) (hy : f y = 0) : ∑ b : { b : H.V // b ≠ y }, f ↑b = ∑ b : H.V, f b

If the marked summand vanishes, summing over the unmarked subtype is the same as summing over the whole factor.

@[simp]

theorem Utilities.deg_wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : CFDiv.degree (wedgeAddDivisor G H x y D E) = CFDiv.degree D + CFDiv.degree E

Degrees add when the marked coefficients are placed at the common vertex.

theorem Utilities.deg_wedgeLiftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : CFDiv.degree (wedgeLiftLeftDivisor G H x y D) = CFDiv.degree D

@[simp]

theorem Utilities.deg_wedgeLiftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (E : CFDiv H) : CFDiv.degree (wedgeLiftRightDivisor G H x y E) = CFDiv.degree E

theorem Utilities.effective_wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (hD : effective D) (hE : effective E) : effective (wedgeAddDivisor G H x y D E)

Effectivity is preserved when two effective divisors are glued.

theorem Utilities.effective_wedgeLiftLeftDivisor_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : effective (wedgeLiftLeftDivisor G H x y D) ↔ effective D

@[simp]

theorem Utilities.effective_wedgeLiftRightDivisor_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (E : CFDiv H) : effective (wedgeLiftRightDivisor G H x y E) ↔ effective E

def Utilities.wedgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (τ : firingScript H) (_hxy : σ x = τ y) : firingScript (vertexWedge G H x y)

Glue firing scripts by requiring their values to agree at the identified vertex.

Equations

• Utilities.wedgeScript G H x y σ τ _hxy = Sum.elim σ fun (b : { b : H.V // b ≠ y }) => τ ↑b

@[simp]

theorem Utilities.wedgeScript_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (τ : firingScript H) (hxy : σ x = τ y) (a : G.V) : wedgeScript G H x y σ τ hxy (Sum.inl a) = σ a

@[simp]

theorem Utilities.wedgeScript_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (τ : firingScript H) (hxy : σ x = τ y) (b : { b : H.V // b ≠ y }) : wedgeScript G H x y σ τ hxy (Sum.inr b) = τ ↑b

theorem Utilities.vertexWedge_edge_card (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : (vertexWedge G H x y).edges.card = G.edges.card + H.edges.card

theorem Utilities.vertexWedge_vertex_card (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : Fintype.card (vertexWedge G H x y).V = Fintype.card G.V + Fintype.card H.V - 1

Identifying one vertex reduces the total vertex count by one.

@[simp]

theorem Utilities.genus_vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : (vertexWedge G H x y).genus = G.genus + H.genus

Vertex identification creates no cycle: genera add across a wedge.

@[simp]

theorem Utilities.num_edges_vertexWedge_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a b : G.V) : numEdges (vertexWedge G H x y) (Sum.inl a) (Sum.inl b) = numEdges G a b

Edge multiplicities between two vertices of the left factor are unchanged by wedging on the right factor.

@[simp]

theorem Utilities.num_edges_vertexWedge_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a b : { z : H.V // z ≠ y }) : numEdges (vertexWedge G H x y) (Sum.inr a) (Sum.inr b) = numEdges H ↑a ↑b

Edge multiplicities between unmarked vertices of the right factor are unchanged by the wedge.

@[simp]

theorem Utilities.num_edges_vertexWedge_marked_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (b : { z : H.V // z ≠ y }) : numEdges (vertexWedge G H x y) (Sum.inl x) (Sum.inr b) = numEdges H y ↑b

The edges from the common vertex to an unmarked right vertex are exactly the edges from the right marked vertex before identification.

@[simp]

theorem Utilities.num_edges_vertexWedge_left_right_of_ne (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) (b : { z : H.V // z ≠ y }) (hax : a ≠ x) : numEdges (vertexWedge G H x y) (Sum.inl a) (Sum.inr b) = 0

A left vertex other than the common vertex has no incident edge in the unmarked part of the right factor.

@[simp]

theorem Utilities.num_edges_vertexWedge_left_right (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) (b : { z : H.V // z ≠ y }) : numEdges (vertexWedge G H x y) (Sum.inl a) (Sum.inr b) = if a = x then numEdges H y ↑b else 0

Cross-edge multiplicities are concentrated at the common left vertex.

@[simp]

theorem Utilities.num_edges_vertexWedge_rightVertex (G : CFGraph) (H : CFGraph) (x : G.V) (y a b : H.V) : numEdges (vertexWedge G H x y) (wedgeRightVertex G H x y a) (wedgeRightVertex G H x y b) = numEdges H a b

Identifying the marked vertices preserves every edge multiplicity from the right factor (including those incident to the marked vertex).

theorem Utilities.prin_wedgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (τ : firingScript H) (hxy : σ x = τ y) : (prin (vertexWedge G H x y)) (wedgeScript G H x y σ τ hxy) = wedgeAddDivisor G H x y ((prin G) σ) ((prin H) τ)

Compatible firing scripts glue to the sum of their principal divisors.

theorem Utilities.prin_const_script (G : CFGraph) (c : ℤ) : ((prin G) fun (x : G.V) => c) = 0

A constant firing script has zero principal divisor.

def Utilities.shiftScript (G : CFGraph) (σ : firingScript G) (c : ℤ) : firingScript G

Add a constant to a firing script. This changes no principal divisor.

Equations

• Utilities.shiftScript G σ c v = σ v + c

@[simp]

theorem Utilities.shiftScript_apply (G : CFGraph) (σ : firingScript G) (c : ℤ) (v : G.V) : shiftScript G σ c v = σ v + c

@[simp]

theorem Utilities.prin_shiftScript (G : CFGraph) (σ : firingScript G) (c : ℤ) : (prin G) (shiftScript G σ c) = (prin G) σ

theorem Utilities.linear_equiv_wedgeAddDivisor_of_prin (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D D' : CFDiv G) (E E' : CFDiv H) (σ : firingScript G) (τ : firingScript H) (hxy : σ x = τ y) (hG : (prin G) σ = D' - D) (hH : (prin H) τ = E' - E) : linearEquiv (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) (wedgeAddDivisor G H x y D' E')

Compatible principal witnesses transport linear equivalence to a wedge.

theorem Utilities.linear_equiv_wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D D' : CFDiv G) (E E' : CFDiv H) (hG : linearEquiv G D D') (hH : linearEquiv H E E') : linearEquiv (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) (wedgeAddDivisor G H x y D' E')

Linear equivalence on both factors transports to the wedge. The proof normalizes the right firing script by a constant so that the two scripts agree at the identified vertex.

theorem Utilities.winnable_wedgeAddDivisor_of_prin (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D D' : CFDiv G) (E E' : CFDiv H) (σ : firingScript G) (τ : firingScript H) (hxy : σ x = τ y) (hG : (prin G) σ = D' - D) (hH : (prin H) τ = E' - E) (hD' : effective D') (hE' : effective E') : winnable (vertexWedge G H x y) (wedgeAddDivisor G H x y D E)

A compatible pair of effective representatives makes the glued divisor winnable.

theorem Utilities.winnable_wedgeAddDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (hD : winnable G D) (hE : winnable H E) : winnable (vertexWedge G H x y) (wedgeAddDivisor G H x y D E)

Winnability transports from the two factors to their vertex wedge.

theorem Utilities.winnable_add_effective_divisor (G : CFGraph) (D E : CFDiv G) (hD : winnable G D) (hE : effective E) : winnable G (D + E)

Adding an effective divisor preserves winnability.

theorem Utilities.winnable_of_rank_ge_one (G : CFGraph) (D : CFDiv G) (hD : rank G D ≥ 1) : winnable G D

A rank-one divisor is winnable.

theorem Utilities.rank_vertexWedge_ge_one (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (hD : rank G D ≥ 1) (hE : rank H E ≥ 1) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ 1

Rank-one divisors on the two factors glue to a rank-one divisor on their vertex wedge, without the degree correction needed for a bridge.

theorem Utilities.BNExists_vertexWedge_rank_one (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (d₁ d₂ : ℤ) (hG : BNExists G 1 d₁) (hH : BNExists H 1 d₂) : BNExists (vertexWedge G H x y) 1 (d₁ + d₂)

Rank-one Brill--Noether witnesses glue across a vertex sum with degrees adding exactly.

def Utilities.restrictLeftWedgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : firingScript G

Restrict a wedge firing script to the left factor.

Equations

• Utilities.restrictLeftWedgeScript G H x y σ a = σ (Sum.inl a)

def Utilities.restrictRightWedgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : firingScript H

Restrict a wedge firing script to the right factor, reading the common vertex at y.

Equations

• Utilities.restrictRightWedgeScript G H x y σ b = σ (Utilities.wedgeRightVertex G H x y b)

@[simp]

theorem Utilities.restrictLeftWedgeScript_apply (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) (a : G.V) : restrictLeftWedgeScript G H x y σ a = σ (Sum.inl a)

@[simp]

theorem Utilities.restrictRightWedgeScript_apply (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) (b : H.V) : restrictRightWedgeScript G H x y σ b = σ (wedgeRightVertex G H x y b)

@[simp]

theorem Utilities.restrictWedgeScripts_agree (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : restrictLeftWedgeScript G H x y σ x = restrictRightWedgeScript G H x y σ y

@[simp]

theorem Utilities.wedgeScript_restrictWedgeScripts (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : wedgeScript G H x y (restrictLeftWedgeScript G H x y σ) (restrictRightWedgeScript G H x y σ) ⋯ = σ

def Utilities.chipShift (G : CFGraph) (D : CFDiv G) (v : G.V) (t : ℤ) : CFDiv G

Add a prescribed integral number of chips at a vertex.

Equations

• Utilities.chipShift G D v t = D + t • oneChip v

@[simp]

theorem Utilities.chipShift_apply (G : CFGraph) (D : CFDiv G) (v w : G.V) (t : ℤ) : chipShift G D v t w = D w + if w = v then t else 0

theorem Utilities.linear_equiv_chipShift_of_prin (G : CFGraph) (D : CFDiv G) (σ : firingScript G) (v : G.V) (t : ℤ) : linearEquiv G (chipShift G D v t) (chipShift G (D + (prin G) σ) v t)

Principal shifts of a divisor remain linearly equivalent after adding the same chip shift to both representatives.

theorem Utilities.wedgeAddDivisor_chipShift_cancel (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (t : ℤ) : wedgeAddDivisor G H x y (chipShift G D x t) (chipShift H E y (-t)) = wedgeAddDivisor G H x y D E

Opposite chip shifts at the identified vertices cancel in a wedge sum.

theorem Utilities.winnable_vertexWedge_iff_exists_chipShift (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : winnable (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ↔ ∃ (t : ℤ), winnable G (chipShift G D x t) ∧ winnable H (chipShift H E y (-t))

Exact winnability convolution across a vertex wedge. The integer t records how much of the common coefficient is allocated to the left factor.

theorem Utilities.graph_connected_vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (hG : graphConnected G) (hH : graphConnected H) : graphConnected (vertexWedge G H x y)

Wedging two connected graphs at a vertex produces a connected graph.