Canonical divisors on positive subdivisions

The canonical coefficient at a core vertex is its incidence degree minus two; every subdivision-interior coefficient is zero. Thus leaflessness can be checked on the finite core. Degree and rank depend only on the numbers of core vertices and slots. In particular a connected specification with one more slot than core vertices has a canonical divisor of degree two and rank one.

The valence calculations are reused from Utilities.Gluing.CycleRigidity. All statements here concern positive SubdivisionGraph.Spec objects, not contracted zero-length faces.

theorem Utilities.rank_canonical_divisor_eq_genus_sub_one {G : CFGraph} (hConnected : graphConnected G) : rank G (canonicalDivisor G) = G.genus - 1

Riemann--Roch gives the canonical divisor rank on every connected graph.

theorem Utilities.Certificate.SubdivisionGraph.Spec.vertex_degree_coreVertex_eq_incidenceDegree {n p : ℕ} (spec : Spec n p) (v : Fin n) : vertexDegree spec.graph (spec.coreVertex v) = ↑(spec.core.incidenceDegree v)

The graph valence of a core vertex is its occurrence-sensitive incidence degree. Parallel slots are counted separately.

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.canonical_divisor_coreVertex {n p : ℕ} (spec : Spec n p) (v : Fin n) : canonicalDivisor spec.graph (spec.coreVertex v) = ↑(spec.core.incidenceDegree v) - 2

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.canonical_divisor_interiorVertex {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : canonicalDivisor spec.graph (spec.interiorVertex edge offset) = 0

theorem Utilities.Certificate.SubdivisionGraph.Spec.canonical_divisor_effective_iff {n p : ℕ} (spec : Spec n p) : effective (canonicalDivisor spec.graph) ↔ ∀ (v : Fin n), 2 ≤ spec.core.incidenceDegree v

An effective canonical divisor on a positive subdivision is exactly the condition that every core incidence degree is at least two.

theorem Utilities.Certificate.SubdivisionGraph.Spec.canonical_divisor_effective {n p : ℕ} (spec : Spec n p) (hLeafless : ∀ (v : Fin n), 2 ≤ spec.core.incidenceDegree v) : effective (canonicalDivisor spec.graph)

Core leaflessness makes the canonical divisor effective, uniformly in all positive edge lengths.

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.deg_canonical_divisor {n p : ℕ} (spec : Spec n p) : CFDiv.degree (canonicalDivisor spec.graph) = 2 * (↑p - ↑n)

The canonical degree is determined by the finite core counts.

theorem Utilities.Certificate.SubdivisionGraph.Spec.rank_canonical_divisor {n p : ℕ} (spec : Spec n p) (hConnected : graphConnected spec.graph) : rank spec.graph (canonicalDivisor spec.graph) = ↑p - ↑n

On a connected positive subdivision, the canonical rank is determined by the finite core counts.

theorem Utilities.Certificate.SubdivisionGraph.Spec.deg_canonical_divisor_eq_two {n p : ℕ} (spec : Spec n p) (hGenusTwo : p = n + 1) : CFDiv.degree (canonicalDivisor spec.graph) = 2

One more slot than core vertices gives canonical degree two.

theorem Utilities.Certificate.SubdivisionGraph.Spec.rank_canonical_divisor_eq_one {n p : ℕ} (spec : Spec n p) (hConnected : graphConnected spec.graph) (hGenusTwo : p = n + 1) : rank spec.graph (canonicalDivisor spec.graph) = 1

The canonical divisor of a connected genus-two subdivision has rank one, including every connected Spec 4 5.

theorem Utilities.Certificate.SubdivisionGraph.Spec.effective_canonical_pencil {n p : ℕ} (spec : Spec n p) (hConnected : graphConnected spec.graph) (hGenusTwo : p = n + 1) (hLeafless : ∀ (v : Fin n), 2 ≤ spec.core.incidenceDegree v) : effective (canonicalDivisor spec.graph) ∧ CFDiv.degree (canonicalDivisor spec.graph) = 2 ∧ rank spec.graph (canonicalDivisor spec.graph) ≥ 1

Package the effective canonical pencil needed for a leafless genus-two factor in a gluing construction.