Weierstrass partitions of pointed divisors

This file formalizes the pole orders and Weierstrass partition used in Definition 1.6 and Proposition 6.10 of the twice-marked banana paper.

The definition is degree-independent. For a divisor D on a connected pointed graph (G, v), the ith pole order is the least integer ell for which rank (D + ell * v) >= i; the ith part is

i + genus G - deg D - poleOrder G v D i.

Riemann--Roch supplies an upper bound on the pole order, while the elementary rank--degree inequality supplies a lower bound, so the integer infimum really is a minimum. The parts are weakly decreasing and vanish from row genus G onward, hence define an honest finite YoungDiagram.

def Bananas.poleOrderSet (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : Set ℤ

The integers at which the pointed rank has reached row i.

Equations

• Bananas.poleOrderSet G v D i = {ell : ℤ | ↑i ≤ rank G (D + ell • oneChip v)}

noncomputable def Bananas.poleOrder (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℤ

Definition 1.6: the least twist at the marked point having rank at least i.

Equations

• Bananas.poleOrder G v D i = sInf (Bananas.poleOrderSet G v D i)

theorem Bananas.poleOrderSet_nonempty {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : (poleOrderSet G v D i).Nonempty

theorem Bananas.poleOrderSet_bddBelow (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : BddBelow (poleOrderSet G v D i)

theorem Bananas.poleOrder_mem_set {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : poleOrder G v D i ∈ poleOrderSet G v D i

theorem Bananas.poleOrder_rank_ge {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : ↑i ≤ rank G (D + poleOrder G v D i • oneChip v)

theorem Bananas.poleOrder_le_of_rank_ge {G : CFGraph} (_hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) (ell : ℤ) (hRank : ↑i ≤ rank G (D + ell • oneChip v)) : poleOrder G v D i ≤ ell

theorem Bananas.rank_lt_of_lt_poleOrder {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) (ell : ℤ) (hell : ell < poleOrder G v D i) : rank G (D + ell • oneChip v) < ↑i

theorem Bananas.poleOrder_le_riemannRoch {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : poleOrder G v D i ≤ ↑i + G.genus - CFDiv.degree D

theorem Bananas.rank_poleOrder_eq {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : rank G (D + poleOrder G v D i • oneChip v) = ↑i

The rank at the least pole order is exactly the row index.

theorem Bananas.rank_poleOrder_sub_one_eq {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : rank G (D + (poleOrder G v D i - 1) • oneChip v) = ↑i - 1

Immediately before the ith pole, the rank is i - 1.

theorem Bananas.poleOrder_eq_of_rank_crossing {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) (ell : ℤ) (hAt : ↑i ≤ rank G (D + ell • oneChip v)) (hBefore : rank G (D + (ell - 1) • oneChip v) < ↑i) : poleOrder G v D i = ell

A one-step rank crossing characterizes the corresponding pole order.

theorem Bananas.poleOrder_strictMono {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : StrictMono (poleOrder G v D)

Pole orders are strictly increasing with the rank row.

theorem Bananas.poleOrder_succ_le {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : poleOrder G v D i + 1 ≤ poleOrder G v D (i + 1)

Consecutive pole orders differ by at least one.

noncomputable def Bananas.weierstrassPartInt (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℤ

The integer underlying the ith Weierstrass part.

Equations

• Bananas.weierstrassPartInt G v D i = ↑i + G.genus - CFDiv.degree D - Bananas.poleOrder G v D i

theorem Bananas.weierstrassPartInt_nonneg {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : 0 ≤ weierstrassPartInt G v D i

noncomputable def Bananas.weierstrassPart (G : CFGraph) (v : G.V) (D : CFDiv G) (i : ℕ) : ℕ

Definition 1.6: the ith part of the Weierstrass partition.

Equations

• Bananas.weierstrassPart G v D i = (Bananas.weierstrassPartInt G v D i).toNat

theorem Bananas.weierstrassPart_cast {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : ↑(weierstrassPart G v D i) = weierstrassPartInt G v D i

theorem Bananas.weierstrassPart_anti {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) {i j : ℕ} (hij : i ≤ j) : weierstrassPart G v D j ≤ weierstrassPart G v D i

theorem Bananas.poleOrder_eq_riemannRoch_of_genus_le {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) (hi : G.genus.toNat ≤ i) : poleOrder G v D i = ↑i + G.genus - CFDiv.degree D

@[simp]

theorem Bananas.weierstrassPart_eq_zero_of_genus_le {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) (hi : G.genus.toNat ≤ i) : weierstrassPart G v D i = 0

noncomputable def Bananas.weierstrassRowLens (G : CFGraph) (v : G.V) (D : CFDiv G) : List ℕ

The finite row-list of the Weierstrass partition. Zero trailing rows are harmless to YoungDiagram.ofRowLens.

Equations

• Bananas.weierstrassRowLens G v D = List.map (Bananas.weierstrassPart G v D) (List.range G.genus.toNat)

theorem Bananas.weierstrassRowLens_sorted {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : (weierstrassRowLens G v D).SortedGE

noncomputable def Bananas.weierstrassPartition {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : YoungDiagram

Definition 1.6 as an actual finite Young diagram.

Equations

• Bananas.weierstrassPartition hG v D = YoungDiagram.ofRowLens (Bananas.weierstrassRowLens G v D) ⋯

theorem Bananas.onceMarkedPart_eq_rowLen (lambda : YoungDiagram) (i : ℕ) : Utilities.onceMarkedPart lambda i = lambda.rowLen i

onceMarkedPart is simply the row length of a Young diagram, including the zero extension beyond its positive rows.

theorem Bananas.weierstrassPartition_rowLen {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : (weierstrassPartition hG v D).rowLen i = weierstrassPart G v D i

theorem Bananas.weierstrassPartition_part {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (i : ℕ) : Utilities.onceMarkedPart (weierstrassPartition hG v D) i = weierstrassPart G v D i

noncomputable def Bananas.weierstrassSize {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : ℕ

Definition 1.6: the finite size |lambda(D,v)|.

Equations

• Bananas.weierstrassSize hG v D = (Bananas.weierstrassPartition hG v D).card

theorem Bananas.weierstrassSize_eq_sum {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : weierstrassSize hG v D = ∑ i ∈ Finset.range G.genus.toNat, weierstrassPart G v D i

theorem Bananas.onceMarkedCensusContains_weierstrassPartition {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) : Utilities.OnceMarkedCensusContains G v (weierstrassPartition hG v D)

The Weierstrass partition of D is literally an element of the once-marked divisor census, witnessed by D itself.

theorem Bananas.census_partition_le_weierstrassPartition {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (D : CFDiv G) (lambda : YoungDiagram) (hRows : ∀ (i : ℕ), rank G (D + (↑i + G.genus - CFDiv.degree D - ↑(Utilities.onceMarkedPart lambda i)) • oneChip v) ≥ ↑i) : lambda ≤ weierstrassPartition hG v D

A census partition witnessed by D is contained in the actual Weierstrass partition of D. This is the monotonicity bridge needed in Section 6: the census definition asks only for a rank lower bound at each row, whereas pole orders record the least such twist.

theorem Bananas.census_card_le_weierstrassSize {G : CFGraph} (hG : _root_.graphConnected G) (v : G.V) (lambda : YoungDiagram) (hCensus : Utilities.OnceMarkedCensusContains G v lambda) : lambda.card ≤ weierstrassSize hG v (Classical.choose hCensus)

Consequently every census partition is no larger than the Weierstrass partition of its witness divisor.