Divisors and firing scripts on a bridge graph

Divisors and firing scripts on either factor extend by zero to the graph formed by joining the factors with a bridge. A script which is one on the left factor and zero on the right records the elementary chip transfer across the bridge.

def MarkedGraphs.liftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : CFDiv (Utilities.bridgeGraph G H x y)

Extend a divisor on the left factor by zero on the right factor.

Equations

• MarkedGraphs.liftLeftDivisor G H x y D = Sum.elim D fun (x : H.V) => 0

def MarkedGraphs.liftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) : CFDiv (Utilities.bridgeGraph G H x y)

Extend a divisor on the right factor by zero on the left factor.

Equations

• MarkedGraphs.liftRightDivisor G H x y D = Sum.elim (fun (x : G.V) => 0) D

@[simp]

theorem MarkedGraphs.liftLeftDivisor_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (a : G.V) : liftLeftDivisor G H x y D (Sum.inl a) = D a

@[simp]

theorem MarkedGraphs.liftLeftDivisor_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (b : H.V) : liftLeftDivisor G H x y D (Sum.inr b) = 0

@[simp]

theorem MarkedGraphs.liftRightDivisor_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) (a : G.V) : liftRightDivisor G H x y D (Sum.inl a) = 0

@[simp]

theorem MarkedGraphs.liftRightDivisor_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) (b : H.V) : liftRightDivisor G H x y D (Sum.inr b) = D b

@[simp]

theorem MarkedGraphs.deg_liftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : CFDiv.degree (liftLeftDivisor G H x y D) = CFDiv.degree D

Zero extension from the left preserves divisor degree.

@[simp]

theorem MarkedGraphs.deg_liftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) : CFDiv.degree (liftRightDivisor G H x y D) = CFDiv.degree D

Zero extension from the right preserves divisor degree.

@[simp]

theorem MarkedGraphs.effective_liftLeftDivisor_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : effective (liftLeftDivisor G H x y D) ↔ effective D

Zero extension from the left is effective exactly when the original divisor is effective.

@[simp]

theorem MarkedGraphs.effective_liftRightDivisor_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) : effective (liftRightDivisor G H x y D) ↔ effective D

Zero extension from the right is effective exactly when the original divisor is effective.

def MarkedGraphs.liftLeftScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) : firingScript (Utilities.bridgeGraph G H x y)

Extend a firing script on the left factor by zero on the right.

Equations

• MarkedGraphs.liftLeftScript G H x y σ = Sum.elim σ fun (x : H.V) => 0

def MarkedGraphs.liftRightScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) : firingScript (Utilities.bridgeGraph G H x y)

Extend a firing script on the right factor by zero on the left.

Equations

• MarkedGraphs.liftRightScript G H x y σ = Sum.elim (fun (x : G.V) => 0) σ

@[simp]

theorem MarkedGraphs.liftLeftScript_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (a : G.V) : liftLeftScript G H x y σ (Sum.inl a) = σ a

@[simp]

theorem MarkedGraphs.liftLeftScript_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (b : H.V) : liftLeftScript G H x y σ (Sum.inr b) = 0

@[simp]

theorem MarkedGraphs.liftRightScript_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) (a : G.V) : liftRightScript G H x y σ (Sum.inl a) = 0

@[simp]

theorem MarkedGraphs.liftRightScript_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) (b : H.V) : liftRightScript G H x y σ (Sum.inr b) = σ b

def MarkedGraphs.extendLeftScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) : firingScript (Utilities.bridgeGraph G H x y)

Extend a left-factor script constantly across the right factor, using its value at the bridge endpoint. This introduces no firing across the bridge.

Equations

• MarkedGraphs.extendLeftScript G H x y σ = Sum.elim σ fun (x_1 : H.V) => σ x

def MarkedGraphs.extendRightScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) : firingScript (Utilities.bridgeGraph G H x y)

Extend a right-factor script constantly across the left factor, using its value at the bridge endpoint. This introduces no firing across the bridge.

Equations

• MarkedGraphs.extendRightScript G H x y σ = Sum.elim (fun (x : G.V) => σ y) σ

@[simp]

theorem MarkedGraphs.extendLeftScript_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (a : G.V) : extendLeftScript G H x y σ (Sum.inl a) = σ a

@[simp]

theorem MarkedGraphs.extendLeftScript_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) (b : H.V) : extendLeftScript G H x y σ (Sum.inr b) = σ x

@[simp]

theorem MarkedGraphs.extendRightScript_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) (a : G.V) : extendRightScript G H x y σ (Sum.inl a) = σ y

@[simp]

theorem MarkedGraphs.extendRightScript_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) (b : H.V) : extendRightScript G H x y σ (Sum.inr b) = σ b

theorem MarkedGraphs.prin_extendLeftScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript G) : (prin (Utilities.bridgeGraph G H x y)) (extendLeftScript G H x y σ) = liftLeftDivisor G H x y ((prin G) σ)

Endpoint-constant extension carries a principal divisor from the left factor to its zero extension on the bridge graph.

theorem MarkedGraphs.prin_extendRightScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript H) : (prin (Utilities.bridgeGraph G H x y)) (extendRightScript G H x y σ) = liftRightDivisor G H x y ((prin H) σ)

Endpoint-constant extension carries a principal divisor from the right factor to its zero extension on the bridge graph.

theorem MarkedGraphs.linear_equiv_liftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D E : CFDiv G} (hDE : linearEquiv G D E) : linearEquiv (Utilities.bridgeGraph G H x y) (liftLeftDivisor G H x y D) (liftLeftDivisor G H x y E)

Linear equivalence on the left factor remains linear equivalence after zero extension to the bridge graph.

theorem MarkedGraphs.linear_equiv_liftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D E : CFDiv H} (hDE : linearEquiv H D E) : linearEquiv (Utilities.bridgeGraph G H x y) (liftRightDivisor G H x y D) (liftRightDivisor G H x y E)

Linear equivalence on the right factor remains linear equivalence after zero extension to the bridge graph.

theorem MarkedGraphs.winnable_liftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D : CFDiv G} (hD : winnable G D) : winnable (Utilities.bridgeGraph G H x y) (liftLeftDivisor G H x y D)

Winnability on the left factor is preserved by zero extension.

theorem MarkedGraphs.winnable_liftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D : CFDiv H} (hD : winnable H D) : winnable (Utilities.bridgeGraph G H x y) (liftRightDivisor G H x y D)

Winnability on the right factor is preserved by zero extension.

def MarkedGraphs.leftSideIndicator (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : firingScript (Utilities.bridgeGraph G H x y)

The firing script which is one on the left factor and zero on the right.

Equations

• MarkedGraphs.leftSideIndicator G H x y = MarkedGraphs.liftLeftScript G H x y fun (x : G.V) => 1

@[simp]

theorem MarkedGraphs.leftSideIndicator_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (a : G.V) : leftSideIndicator G H x y (Sum.inl a) = 1

@[simp]

theorem MarkedGraphs.leftSideIndicator_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y b : H.V) : leftSideIndicator G H x y (Sum.inr b) = 0

theorem MarkedGraphs.prin_leftSideIndicator (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : (prin (Utilities.bridgeGraph G H x y)) (leftSideIndicator G H x y) = oneChip (Sum.inr y) - oneChip (Sum.inl x)

With the library's negative-Laplacian sign convention, firing the left side once moves one chip from the left endpoint to the right endpoint.