Rank one across a bridge

Rank-one divisors on two factors combine to a rank-one divisor on their bridge sum after removing one chip at a bridge endpoint. The loss of one degree is the familiar bridge gluing correction.

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

Zero extension from the left commutes with subtracting one chip.

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

Zero extension from the right commutes with subtracting one chip.

theorem MarkedGraphs.winnable_add_liftDivisors (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 (Utilities.bridgeGraph G H x y) (liftLeftDivisor G H x y D + liftRightDivisor G H x y E)

Winnable divisors on the two factors have a winnable sum after zero extension to the bridge graph.

theorem MarkedGraphs.linear_equiv_sub_bridge_endpoints (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (P : CFDiv (Utilities.bridgeGraph G H x y)) : linearEquiv (Utilities.bridgeGraph G H x y) (P - oneChip (Sum.inr y)) (P - oneChip (Sum.inl x))

Subtracting the right bridge-end chip is linearly equivalent to subtracting the left bridge-end chip.

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

The divisor obtained by gluing D and E across the bridge and removing one chip at the left bridge endpoint.

Equations

• MarkedGraphs.bridgeRankOneDivisor G H x y D E = MarkedGraphs.liftLeftDivisor G H x y D + MarkedGraphs.liftRightDivisor G H x y E - oneChip (Sum.inl x)

theorem MarkedGraphs.rank_bridgeGraph_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 (Utilities.bridgeGraph G H x y) (liftLeftDivisor G H x y D + liftRightDivisor G H x y E - oneChip (Sum.inl x)) ≥ 1

Rank-one divisors on two factors glue to a rank-one divisor of degree one less than the sum of their degrees.

theorem MarkedGraphs.rank_bridgeRankOneDivisor_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 (Utilities.bridgeGraph G H x y) (bridgeRankOneDivisor G H x y D E) ≥ 1

The named bridge divisor has rank at least one whenever both factor divisors do.

theorem MarkedGraphs.deg_bridgeRankOneDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) : CFDiv.degree (bridgeRankOneDivisor G H x y D E) = CFDiv.degree D + CFDiv.degree E - 1

The glued rank-one candidate has the expected corrected degree.

theorem MarkedGraphs.BNExists_bridgeGraph_rank_one (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) {d₁ d₂ : ℤ} (hG : Utilities.BNExists G 1 d₁) (hH : Utilities.BNExists H 1 d₂) : Utilities.BNExists (Utilities.bridgeGraph G H x y) 1 (d₁ + d₂ - 1)

Rank-one Brill--Noether witnesses glue across a bridge with the expected loss of one degree.