Endpoint transmission on banana graphs

This file proves the abstract existence/periodicity facts for transmission permutations from the rank slipface. The endpoint-specific rank calculation and inversion count are developed separately from this generic layer.

noncomputable def Bananas.rankSlipFunction (M : TwiceMarked) (D : CFDiv M.graph) : ℤ → ℤ → ℤ

Divisor rank after adding chips at the first mark and removing them at the second, plus one.

Equations

• Bananas.rankSlipFunction M D a b = rank M.graph (D + a • oneChip M.u - b • oneChip M.v) + 1

noncomputable def Bananas.rankSlipFace (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) : SlipFace

The rank function of a twice-marked divisor, shifted by one, is a slipface.

Equations

• Bananas.rankSlipFace M D hconn = Classical.choose ⋯

@[simp]

theorem Bananas.rankSlipFace_apply (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) (a b : ℤ) : (rankSlipFace M D hconn).func a b = rank M.graph (D + a • oneChip M.u - b • oneChip M.v) + 1

@[simp]

theorem Bananas.rankSlipFace_chi (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) : (rankSlipFace M D hconn).χ = CFDiv.degree D - M.graph.genus + 1

theorem Bananas.rankSlipFace_Delta (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) (a b : ℤ) : (rankSlipFace M D hconn).Δ a b = rankDelta M (D + (a + 1) • oneChip M.u - b • oneChip M.v)

theorem Bananas.exists_transmissionPermutation_of_submodular (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) (hD : Submodular M D) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation M D τ

Submodularity recovers the transmission permutation of a divisor.

theorem Bananas.rankDelta_eq_of_linearEquiv {M : TwiceMarked} {D E : CFDiv M.graph} (hDE : linearEquiv M.graph D E) : rankDelta M D = rankDelta M E

theorem Bananas.rankDelta_marked_twist_add_torsion {M : TwiceMarked} {k : ℕ} (hk : TorsionWitness M k) (D : CFDiv M.graph) (a b : ℤ) : rankDelta M (D + (a + ↑k) • oneChip M.u - (b + ↑k) • oneChip M.v) = rankDelta M (D + a • oneChip M.u - b • oneChip M.v)

theorem Bananas.exists_affineTransmissionPermutation_of_submodular (M : TwiceMarked) (D : CFDiv M.graph) (hconn : graphConnected M.graph) {k : ℕ} (hD : Submodular M D) (hk : TorsionWitness M k) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation M D τ ∧ IsKAffine k τ

A transmission permutation recovered from a submodular divisor is affine at every torsion witness.

The endpoint pencil

theorem Bananas.banana_graph_connected {g : ℕ} (B : Banana g) : graphConnected (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

theorem Bananas.banana_genus {g : ℕ} (B : Banana g) : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).genus = ↑g

def Bananas.endpointPencilDivisor {g : ℕ} (B : Banana g) : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The literal divisor consisting of one chip at each multivalent endpoint.

Equations

• Bananas.endpointPencilDivisor B = oneChip (Bananas.leftEndpoint B) + oneChip (Bananas.rightEndpoint B)

@[simp]

theorem Bananas.degree_endpointPencilDivisor {g : ℕ} (B : Banana g) : CFDiv.degree (endpointPencilDivisor B) = 2

theorem Bananas.rank_endpointPencilDivisor_ge_one {g : ℕ} (B : Banana g) : 1 ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (endpointPencilDivisor B)

The literal endpoint divisor (not merely some divisor supplied by BNExists) has rank at least one.

theorem Bananas.rank_add_ge_add_rank (G : CFGraph) (D E : CFDiv G) (hD : 0 ≤ rank G D) (hE : 0 ≤ rank G E) : rank G (D + E) ≥ rank G D + rank G E

Public form of rank superadditivity. The dependency proves this internally for Clifford's theorem but keeps that lemma private.

theorem Bananas.rank_endpointPencil_nsmul_ge {g : ℕ} (B : Banana g) (b : ℕ) : ↑b ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (b • endpointPencilDivisor B)

Every positive multiple of the endpoint pencil has at least the expected hyperelliptic rank.

theorem Bananas.rank_endpointPencil_nsmul_eq {g : ℕ} (B : Banana g) (b : ℕ) (hb : b ≤ g) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (b • endpointPencilDivisor B) = ↑b

Up through the genus, the b-fold endpoint pencil has rank exactly b.

theorem Bananas.rank_endpointPencil_nsmul_sub_left_eq {g : ℕ} (B : Banana g) (b : ℕ) (hbPos : 0 < b) (hb : b ≤ g) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (b • endpointPencilDivisor B - oneChip (leftEndpoint B)) = ↑b - 1

theorem Bananas.rank_endpointPencil_nsmul_sub_right_eq {g : ℕ} (B : Banana g) (b : ℕ) (hbPos : 0 < b) (hb : b ≤ g) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (b • endpointPencilDivisor B - oneChip (rightEndpoint B)) = ↑b - 1

theorem Bananas.rankDelta_endpointPencil_nsmul_eq_one {g : ℕ} (B : Banana g) (b : ℕ) (hb : b ≤ g) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) (b • endpointPencilDivisor B) = 1

The marked rank second difference of every endpoint-pencil multiple up to the genus is one. This is the rank calculation which produces the decreasing endpoint block in the transmission permutation.