Contracting a separating bridge

Contracting the bridge in bridgeGraph G H x y gives the vertex wedge vertexWedge G H x y. This file proves the divisor-theoretic statement behind that observation: merging the two bridge-endpoint coefficients preserves degree, linear equivalence, winnability, and every rank condition.

The proofs are entirely at the level of divisors and firing scripts. In particular, no graph isomorphism or connectivity hypothesis is needed.

The declarations remain in the established MarkedGraphs namespace for API compatibility.

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

Contract the bridge endpoints, using the left endpoint as the vertex of the resulting wedge.

Equations

• Utilities.contractBridgeVertex G H x y = Sum.elim Sum.inl (Utilities.wedgeRightVertex G H x y)

@[simp]

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

@[simp]

theorem Utilities.contractBridgeVertex_inr_marked (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : contractBridgeVertex G H x y (Sum.inr y) = Sum.inl x

@[simp]

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

def Utilities.bridgePushforwardHom (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFDiv (bridgeGraph G H x y) →+ CFDiv (vertexWedge G H x y)

Push a divisor through bridge contraction. The coefficients at the two bridge endpoints are added; every other coefficient is unchanged.

Equations

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

@[reducible, inline]

abbrev Utilities.bridgePushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFDiv (bridgeGraph G H x y) →+ CFDiv (vertexWedge G H x y)

Divisor pushforward along contraction of the separating bridge.

Equations

• Utilities.bridgePushforward G H x y = Utilities.bridgePushforwardHom G H x y

@[simp]

theorem Utilities.bridgePushforward_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) (a : G.V) : (bridgePushforward G H x y) D (Sum.inl a) = D (Sum.inl a) + if a = x then D (Sum.inr y) else 0

@[simp]

theorem Utilities.bridgePushforward_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) (b : { b : H.V // b ≠ y }) : (bridgePushforward G H x y) D (Sum.inr b) = D (Sum.inr ↑b)

def Utilities.bridgeCanonicalLiftHom (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFDiv (vertexWedge G H x y) →+ CFDiv (bridgeGraph G H x y)

The canonical lift puts the coefficient of the common wedge vertex at the left bridge endpoint and puts zero at the right bridge endpoint.

Equations

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

@[reducible, inline]

abbrev Utilities.bridgeCanonicalLift (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : CFDiv (vertexWedge G H x y) →+ CFDiv (bridgeGraph G H x y)

Canonical lift of a wedge divisor across the contracted bridge.

Equations

• Utilities.bridgeCanonicalLift G H x y = Utilities.bridgeCanonicalLiftHom G H x y

@[simp]

theorem Utilities.bridgeCanonicalLift_inl (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) (a : G.V) : (bridgeCanonicalLift G H x y) D (Sum.inl a) = D (Sum.inl a)

@[simp]

theorem Utilities.bridgeCanonicalLift_inr_marked (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) : (bridgeCanonicalLift G H x y) D (Sum.inr y) = 0

@[simp]

theorem Utilities.bridgeCanonicalLift_inr_unmarked (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) (b : H.V) (hb : b ≠ y) : (bridgeCanonicalLift G H x y) D (Sum.inr b) = D (Sum.inr ⟨b, hb⟩)

@[simp]

theorem Utilities.bridgePushforward_canonicalLift (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) : (bridgePushforward G H x y) ((bridgeCanonicalLift G H x y) D) = D

@[simp]

theorem Utilities.deg_bridgePushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) : CFDiv.degree ((bridgePushforward G H x y) D) = CFDiv.degree D

Bridge contraction preserves divisor degree.

@[simp]

theorem Utilities.deg_bridgeCanonicalLift (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) : CFDiv.degree ((bridgeCanonicalLift G H x y) D) = CFDiv.degree D

The canonical lift also preserves degree.

theorem Utilities.effective_bridgePushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D : CFDiv (bridgeGraph G H x y)} (hD : effective D) : effective ((bridgePushforward G H x y) D)

Pushforward takes effective divisors to effective divisors.

@[simp]

theorem Utilities.effective_bridgeCanonicalLift_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (vertexWedge G H x y)) : effective ((bridgeCanonicalLift G H x y) D) ↔ effective D

A wedge divisor is effective exactly when its canonical lift is.

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

Restrict a firing script on the bridge graph to the left factor.

Equations

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

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

Restrict a firing script on the bridge graph to the right factor.

Equations

• Utilities.restrictRightBridgeScript G H x y σ b = σ (Sum.inr b)

@[simp]

theorem Utilities.restrictLeftBridgeScript_apply (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) (a : G.V) : restrictLeftBridgeScript G H x y σ a = σ (Sum.inl a)

@[simp]

theorem Utilities.restrictRightBridgeScript_apply (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) (b : H.V) : restrictRightBridgeScript G H x y σ b = σ (Sum.inr b)

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

After bridge contraction, normalize the right restriction of a firing script by a constant so that its value at y agrees with the left value at x, then glue the two restrictions.

Equations

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

theorem Utilities.bridge_script_decomposition (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) : MarkedGraphs.extendLeftScript G H x y (restrictLeftBridgeScript G H x y σ) + MarkedGraphs.extendRightScript G H x y (restrictRightBridgeScript G H x y σ) + SMul.smul (σ (Sum.inl x) - σ (Sum.inr y)) (MarkedGraphs.leftSideIndicator G H x y) = shiftScript (bridgeGraph G H x y) σ (σ (Sum.inl x))

Every bridge script is, up to a constant, the sum of its endpoint-constant factor extensions and a multiple of the left-side indicator.

theorem Utilities.prin_bridge_decomposition (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) : (prin (bridgeGraph G H x y)) σ = MarkedGraphs.liftLeftDivisor G H x y ((prin G) (restrictLeftBridgeScript G H x y σ)) + MarkedGraphs.liftRightDivisor G H x y ((prin H) (restrictRightBridgeScript G H x y σ)) + SMul.smul (σ (Sum.inl x) - σ (Sum.inr y)) (oneChip (Sum.inr y) - oneChip (Sum.inl x))

Principal divisors on a bridge split into factor-principal parts plus the single elementary transfer across the bridge.

@[simp]

theorem Utilities.bridgePushforward_liftLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) : (bridgePushforward G H x y) (MarkedGraphs.liftLeftDivisor G H x y D) = wedgeLiftLeftDivisor G H x y D

Pushing a zero-extended left divisor through bridge contraction gives its literal left lift to the wedge.

@[simp]

theorem Utilities.bridgePushforward_liftRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv H) : (bridgePushforward G H x y) (MarkedGraphs.liftRightDivisor G H x y D) = wedgeLiftRightDivisor G H x y D

Pushing a zero-extended right divisor through bridge contraction gives its right lift to the wedge.

@[simp]

theorem Utilities.bridgePushforward_endpoint_difference (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : (bridgePushforward G H x y) (oneChip (Sum.inr y) - oneChip (Sum.inl x)) = 0

The elementary bridge transfer disappears when its two endpoints are identified.

theorem Utilities.wedgeLiftLeft_add_wedgeLiftRight (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : wedgeLiftLeftDivisor G H x y D + wedgeLiftRightDivisor G H x y E = wedgeAddDivisor G H x y D E

The two one-sided wedge lifts add to wedgeAddDivisor.

theorem Utilities.prin_contractBridgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) : (prin (vertexWedge G H x y)) (contractBridgeScript G H x y σ) = wedgeAddDivisor G H x y ((prin G) (restrictLeftBridgeScript G H x y σ)) ((prin H) (restrictRightBridgeScript G H x y σ))

The contracted firing script has exactly the two factor-principal parts.

theorem Utilities.bridgePushforward_prin (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (bridgeGraph G H x y)) : (bridgePushforward G H x y) ((prin (bridgeGraph G H x y)) σ) = (prin (vertexWedge G H x y)) (contractBridgeScript G H x y σ)

Bridge contraction sends every principal divisor to a principal divisor, with an explicit contracted firing script.

theorem Utilities.linear_equiv_bridgeCanonicalLift_pushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) : linearEquiv (bridgeGraph G H x y) D ((bridgeCanonicalLift G H x y) ((bridgePushforward G H x y) D))

Every divisor on the bridge graph is linearly equivalent to the canonical lift of its contraction. The sole correction is a transfer across the bridge, witnessed by leftSideIndicator.

theorem Utilities.linear_equiv_bridgePushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D E : CFDiv (bridgeGraph G H x y)} (hDE : linearEquiv (bridgeGraph G H x y) D E) : linearEquiv (vertexWedge G H x y) ((bridgePushforward G H x y) D) ((bridgePushforward G H x y) E)

Linear equivalence descends through bridge contraction.

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

Pull a firing script on the wedge back to the bridge graph, assigning the common wedge value to both bridge endpoints.

Equations

• Utilities.expandWedgeScript G H x y σ = Sum.elim (fun (a : G.V) => σ (Sum.inl a)) fun (b : H.V) => σ (Utilities.wedgeRightVertex G H x y b)

@[simp]

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

@[simp]

theorem Utilities.expandWedgeScript_inr (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) (b : H.V) : expandWedgeScript G H x y σ (Sum.inr b) = σ (wedgeRightVertex G H x y b)

@[simp]

theorem Utilities.contractBridgeScript_expandWedgeScript (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : contractBridgeScript G H x y (expandWedgeScript G H x y σ) = σ

Contracting an endpoint-compatible lifted script recovers the original wedge script literally.

theorem Utilities.principal_bridgeCanonicalLift_prin (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (σ : firingScript (vertexWedge G H x y)) : (bridgeCanonicalLift G H x y) ((prin (vertexWedge G H x y)) σ) ∈ principalDivisors (bridgeGraph G H x y)

A canonical lift of a principal wedge divisor is principal on the bridge graph.

theorem Utilities.linear_equiv_bridgeCanonicalLift (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {D E : CFDiv (vertexWedge G H x y)} (hDE : linearEquiv (vertexWedge G H x y) D E) : linearEquiv (bridgeGraph G H x y) ((bridgeCanonicalLift G H x y) D) ((bridgeCanonicalLift G H x y) E)

Canonical lift preserves linear equivalence from the wedge to the bridge.

theorem Utilities.linear_equiv_bridge_iff_pushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D E : CFDiv (bridgeGraph G H x y)) : linearEquiv (bridgeGraph G H x y) D E ↔ linearEquiv (vertexWedge G H x y) ((bridgePushforward G H x y) D) ((bridgePushforward G H x y) E)

Linear equivalence on the bridge graph is exactly linear equivalence of the contracted divisors.

theorem Utilities.winnable_bridge_iff_pushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) : winnable (bridgeGraph G H x y) D ↔ winnable (vertexWedge G H x y) ((bridgePushforward G H x y) D)

Winnability is invariant under contraction of a separating bridge.

theorem Utilities.rank_geq_bridge_iff_pushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) (k : ℤ) : rankGeq (bridgeGraph G H x y) D k ↔ rankGeq (vertexWedge G H x y) ((bridgePushforward G H x y) D) k

Every rank inequality is invariant under contraction of a separating bridge.

@[simp]

theorem Utilities.rank_bridgePushforward (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv (bridgeGraph G H x y)) : rank (vertexWedge G H x y) ((bridgePushforward G H x y) D) = rank (bridgeGraph G H x y) D

Baker--Norine rank itself is unchanged by contracting a separating bridge.

theorem Utilities.BNExists_bridge_iff_vertexWedge (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (r d : ℤ) : BNExists (bridgeGraph G H x y) r d ↔ BNExists (vertexWedge G H x y) r d

Brill--Noether existence is invariant under contraction of a separating bridge.