Once-marked Brill--Noether generality under vertex gluing

This file proves Proposition 6.14 (prop:glueMarked) of the paper. The key device is a finite piece of the Weierstrass partition attached to a pointed divisor: its ith row is read from the first twist at which the divisor has rank at least i. Only the first r+1 rows are needed for a wedge divisor of rank r.

The construction is independent of the transmission-permutation identity of Proposition 6.10. It uses only the exact vertex-wedge rank formula and the all-row definition OnceMarkedCensusContains.

Pointed rank thresholds

noncomputable def Bananas.pointedRankThreshold (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : ℤ

The first integral twist at which D has rank at least i. We search from degree zero upward; every earlier twist has negative degree and hence rank -1, so this is also the first twist among all integers.

Equations

• Bananas.pointedRankThreshold G hG D q i = ↑(Nat.find ⋯) - CFDiv.degree D

theorem Bananas.rank_at_pointedRankThreshold_ge (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : rank G (D + pointedRankThreshold G hG D q i • oneChip q) ≥ ↑i

theorem Bananas.pointedRankThreshold_le_of_rank_ge (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) (t : ℤ) (ht : rank G (D + t • oneChip q) ≥ ↑i) : pointedRankThreshold G hG D q i ≤ t

Minimality of the pointed rank threshold among all integral twists.

theorem Bananas.rank_before_pointedRankThreshold_lt (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : rank G (D + (pointedRankThreshold G hG D q i - 1) • oneChip q) < ↑i

Immediately before the threshold, the desired rank has not yet been reached.

theorem Bananas.pointedRankThreshold_succ_le (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : pointedRankThreshold G hG D q i + 1 ≤ pointedRankThreshold G hG D q (i + 1)

Successive pointed rank thresholds are separated by at least one twist. This is the monotonicity that makes the associated row lengths weakly decreasing.

Finite pointed diagrams

noncomputable def Bananas.pointedRowLength (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : ℕ

The ith (truncated) Weierstrass row attached to a pointed divisor.

Equations

• Bananas.pointedRowLength G hG D q i = (↑i + G.genus - CFDiv.degree D - Bananas.pointedRankThreshold G hG D q i).toNat

theorem Bananas.pointedRowLength_anti (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (i : ℕ) : pointedRowLength G hG D q (i + 1) ≤ pointedRowLength G hG D q i

noncomputable def Bananas.finitePointedRows (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (r : ℕ) : List ℕ

The first r+1 pointed rows, sufficient for studying a divisor of rank r on a vertex wedge.

Equations

• Bananas.finitePointedRows G hG D q r = List.ofFn fun (i : Fin (r + 1)) => Bananas.pointedRowLength G hG D q ↑i

theorem Bananas.finitePointedRows_sorted (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (r : ℕ) : (finitePointedRows G hG D q r).SortedGE

noncomputable def Bananas.finitePointedDiagram (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (r : ℕ) : YoungDiagram

The finite Young diagram cut out by the first r+1 pointed rows.

Equations

• Bananas.finitePointedDiagram G hG D q r = YoungDiagram.ofRowLens (Bananas.finitePointedRows G hG D q r) ⋯

theorem Bananas.finitePointedDiagram_card (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (r : ℕ) : (finitePointedDiagram G hG D q r).card = (finitePointedRows G hG D q r).sum

theorem Bananas.finitePointedDiagram_censusContains (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (r : ℕ) : Utilities.OnceMarkedCensusContains G q (finitePointedDiagram G hG D q r)

Every finite pointed diagram belongs to the once-marked divisor census, witnessed by the degree-g normalization of the original divisor.

Proposition 6.14

theorem Bananas.pointedRankThreshold_add_le_zero_of_wedge_rank (G : CFGraph) (H : CFGraph) (hG : graphConnected G) (hH : graphConnected H) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (r : ℕ) (hRank : rank (Utilities.vertexWedge G H x y) (Utilities.wedgeAddDivisor G H x y D E) ≥ ↑r) (i : ℕ) (hi : i ≤ r) : pointedRankThreshold G hG D x i + pointedRankThreshold H hH E y (r - i) ≤ 0

The wedge rank inequality forces complementary pointed thresholds to sum to at most zero.

theorem Bananas.pointedRowLength_add_ge_wedge_width (G : CFGraph) (H : CFGraph) (hG : graphConnected G) (hH : graphConnected H) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (r : ℕ) (hRank : rank (Utilities.vertexWedge G H x y) (Utilities.wedgeAddDivisor G H x y D E) ≥ ↑r) (i : ℕ) (hi : i ≤ r) : G.genus + H.genus - (CFDiv.degree D + CFDiv.degree E) + ↑r ≤ ↑(pointedRowLength G hG D x i) + ↑(pointedRowLength H hH E y (r - i))

Each complementary pair of pointed rows dominates the Brill--Noether rectangle width of the wedge divisor.

theorem Bananas.onceMarkedBrillNoetherGeneral_vertexWedge (G : CFGraph) (H : CFGraph) (hG : graphConnected G) (hH : graphConnected H) (x : G.V) (y : H.V) (hGeneralG : OnceMarkedBrillNoetherGeneral G x) (hGeneralH : OnceMarkedBrillNoetherGeneral H y) : BrillNoetherGeneral (Utilities.vertexWedge G H x y)

Paper Proposition 6.14 (prop:glueMarked).

Gluing the marked vertices of two once-marked Brill--Noether-general connected graphs produces an unmarked Brill--Noether-general graph.