Two-pole joins

This file packages the graph obtained by joining two pointed graphs at two ordered pairs of poles. One cross-edge is installed as a separating bridge; the second is then an addEdge. This presentation exposes the unique seam phase created by the second edge while keeping divisors on the two factors as literal functions on a sum type.

The API is deliberately divisor-generic. sumDivisor combines arbitrary factor divisors, phase records the integral seam orbit, and the canonical specialization identifies the residual of the local canonical sum with the four pole chips. In genus two plus genus two, Riemann--Roch therefore says that the two degree-four candidates have exactly the same rank.

structure Utilities.TwoPole (G : CFGraph) : Type u

A graph equipped with two ordered poles. The poles are allowed to coincide; the two cross-edges of a join are nevertheless loopless because they run between the two summands.

• first : G.V

  The first attachment pole, used for the bridge retained in the lower-genus presentation.

• second : G.V

  The second attachment pole, used for the additional cross-edge in the two-pole join.

@[reducible, inline]

abbrev Utilities.TwoPole.bridge (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFGraph

The lower-genus presentation of a two-pole join: retain only the first cross-edge, which is a separating bridge.

Equations

• Utilities.TwoPole.bridge A B p q = Utilities.bridgeGraph A B p.first q.first

@[reducible, inline]

abbrev Utilities.TwoPole.join (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFGraph

Join two graphs by matching their first poles and their second poles.

Equations

• Utilities.TwoPole.join A B p q = Utilities.addEdge (Utilities.TwoPole.bridge A B p q) (Sum.inl p.second) (Sum.inr q.second) ⋯

theorem Utilities.TwoPole.second_endpoints_ne (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : Sum.inl p.second ≠ Sum.inr q.second

The endpoints of the second cross-edge are distinct, independently of whether either pair of poles coincides within its factor.

def Utilities.TwoPole.sumDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : CFDiv (join A B p q)

Add divisors on the two factors by placing them on the two summands. The same function is a divisor on both bridge and join, since addEdge keeps the vertex type unchanged.

Equations

• Utilities.TwoPole.sumDivisor A B p q D E = Sum.elim D E

@[simp]

theorem Utilities.TwoPole.sumDivisor_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (a : A.V) : sumDivisor A B p q D E (Sum.inl a) = D a

@[simp]

theorem Utilities.TwoPole.sumDivisor_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (b : B.V) : sumDivisor A B p q D E (Sum.inr b) = E b

The seam phase orbit

def Utilities.TwoPole.phase (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv (join A B p q)) (n : ℤ) : CFDiv (join A B p q)

Translate a divisor through the integral seam orbit created by the second cross-edge. This is the phase coordinate that has to be chosen when the one-bridge seed is lifted to a genuine two-pole join.

Equations

• Utilities.TwoPole.phase A B p q D n = D + n • Utilities.seamDivisor (Sum.inl p.second) (Sum.inr q.second)

@[simp]

theorem Utilities.TwoPole.phase_zero (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv (join A B p q)) : phase A B p q D 0 = D

theorem Utilities.TwoPole.phase_add (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv (join A B p q)) (m n : ℤ) : phase A B p q (phase A B p q D m) n = phase A B p q D (m + n)

Phases form an additive integral orbit.

theorem Utilities.TwoPole.deg_phase (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv (join A B p q)) (n : ℤ) : CFDiv.degree (phase A B p q D n) = CFDiv.degree D

theorem Utilities.TwoPole.phase_sumDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (n : ℤ) : phase A B p q (sumDivisor A B p q D E) n = sumDivisor A B p q (D + n • oneChip p.second) (E - n • oneChip q.second)

On a factor sum, changing phase credits the second left pole and debits the second right pole.

theorem Utilities.TwoPole.deg_sumDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : CFDiv.degree (sumDivisor A B p q D E) = CFDiv.degree D + CFDiv.degree E

Degrees add under the literal sum of factor divisors.

@[simp]

theorem Utilities.TwoPole.effective_sumDivisor_iff (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : effective (sumDivisor A B p q D E) ↔ effective D ∧ effective E

Effectivity of a factor sum is exactly factorwise effectivity.

theorem Utilities.TwoPole.vertex_degree_bridge_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (a : A.V) : vertexDegree (bridge A B p q) (Sum.inl a) = vertexDegree A a + if a = p.first then 1 else 0

The degree of a left vertex in the one-bridge presentation.

theorem Utilities.TwoPole.vertex_degree_bridge_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (b : B.V) : vertexDegree (bridge A B p q) (Sum.inr b) = vertexDegree B b + if b = q.first then 1 else 0

The degree of a right vertex in the one-bridge presentation.

theorem Utilities.TwoPole.canonical_divisor_bridge (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : canonicalDivisor (bridge A B p q) = fun (z : A.V ⊕ B.V) => Sum.elim (canonicalDivisor A) (canonicalDivisor B) z + oneChip (Sum.inl p.first) z + oneChip (Sum.inr q.first) z

The canonical divisor of the bridge presentation is the sum of the two factor canonical divisors plus one chip at each bridge endpoint.

def Utilities.TwoPole.boundaryDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFDiv (join A B p q)

The four pole chips, regarded as a divisor on the two-pole join.

Equations

• Utilities.TwoPole.boundaryDivisor A B p q = oneChip (Sum.inl p.first) + oneChip (Sum.inl p.second) + oneChip (Sum.inr q.first) + oneChip (Sum.inr q.second)

def Utilities.TwoPole.canonicalSum (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFDiv (join A B p q)

The sum of the two local canonical divisors, with no pole chips added.

Equations

• Utilities.TwoPole.canonicalSum A B p q = Utilities.TwoPole.sumDivisor A B p q (canonicalDivisor A) (canonicalDivisor B)

theorem Utilities.TwoPole.genus_join (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : (join A B p q).genus = A.genus + B.genus + 1

Adding the second cross-edge creates one cycle.

theorem Utilities.TwoPole.connected_join (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (hA : graphConnected A) (hB : graphConnected B) : graphConnected (join A B p q)

A two-pole join of connected factors is connected.

theorem Utilities.TwoPole.deg_boundaryDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFDiv.degree (boundaryDivisor A B p q) = 4

theorem Utilities.TwoPole.deg_canonicalSum (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : CFDiv.degree (canonicalSum A B p q) = 2 * A.genus + 2 * B.genus - 4

theorem Utilities.TwoPole.canonical_divisor_join (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : canonicalDivisor (join A B p q) = canonicalSum A B p q + boundaryDivisor A B p q

Canonical bookkeeping for a two-pole join. The global canonical divisor is the local canonical sum plus exactly the four pole chips.

theorem Utilities.TwoPole.canonical_sub_canonicalSum (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) : canonicalDivisor (join A B p q) - canonicalSum A B p q = boundaryDivisor A B p q

The four pole chips are literally the canonical complement of the local canonical sum.

theorem Utilities.TwoPole.rank_canonicalSum_sub_rank_boundary (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (hA : graphConnected A) (hB : graphConnected B) : rank (join A B p q) (canonicalSum A B p q) - rank (join A B p q) (boundaryDivisor A B p q) = A.genus + B.genus - 4

General Riemann--Roch comparison between the two canonical halves of a two-pole join.

theorem Utilities.TwoPole.rank_canonicalSum_eq_rank_boundary_of_genus_two (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (hA : graphConnected A) (hGenusA : A.genus = 2) (hB : graphConnected B) (hGenusB : B.genus = 2) : rank (join A B p q) (canonicalSum A B p q) = rank (join A B p q) (boundaryDivisor A B p q)

The genus-two K_A+K_B duality lemma. On a two-pole join of two connected genus-two graphs, the local canonical sum and the four pole chips have equal rank. Thus either one may be used as the unmarked degree-four witness.