Canonical duality for transmission witnesses

Riemann--Roch exchanges the two marks and inverts the ASP permutation. With the row convention used by SatisfiesTransmission, the literal canonical complement is off by one in each marked coordinate. The normalized complement is therefore

K - D + u + v.

It has the degree prescribed by τ⁻¹, and its rows are exactly those required for τ⁻¹ at the swapped marks.

def Utilities.transmissionDualDivisor {G : CFGraph} (u v : G.V) (D : CFDiv G) : CFDiv G

The marked normalization of the canonical complement appropriate to transmission duality.

Equations

• Utilities.transmissionDualDivisor u v D = canonicalDivisor G - D + oneChip u + oneChip v

theorem Utilities.degree_transmissionDualDivisor {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) : CFDiv.degree (transmissionDualDivisor u v D) = G.genus + τ⁻¹.χ

The normalized canonical complement has the degree prescribed by the inverse ASP permutation.

theorem Utilities.transmissionDualDivisor_twist {G : CFGraph} (u v : G.V) (D : CFDiv G) (a b : ℤ) : transmissionDualDivisor u v D + a • oneChip v - b • oneChip u = canonicalDivisor G - (D + (b - 1) • oneChip u - (a + 1) • oneChip v)

The complementary marked twist is the canonical complement of the original twist at the transposed, shifted lattice point.

theorem Utilities.transmissionDualDivisor_rank_ge {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (transmissionDualDivisor u v D + a • oneChip v - b • oneChip u) ≥ τ⁻¹.s.func (a + 1) b - 1

The dual row bound supplied by Riemann--Roch.

theorem Utilities.satisfiesTransmission_dual {G : CFGraph} (hconn : graphConnected G) {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) : SatisfiesTransmission G v u τ⁻¹ (transmissionDualDivisor u v D)

A transmission witness canonically yields an inverse-permutation witness at the swapped marks.

theorem Utilities.transmissionExists_dual {G : CFGraph} (hconn : graphConnected G) (u v : G.V) (τ : AspPerm) : TransmissionExists G u v τ → TransmissionExists G v u τ⁻¹

Transmission existence is preserved by Riemann--Roch duality, inversion, and swapping the marked points.

theorem Utilities.transmissionExists_dual_iff {G : CFGraph} (hconn : graphConnected G) (u v : G.V) (τ : AspPerm) : TransmissionExists G v u τ⁻¹ ↔ TransmissionExists G u v τ

The duality transport is an equivalence after applying it twice.