Global geometry of banana graphs

This file records structural facts about bananas which follow directly from their presentation as positive subdivisions of a two-vertex parallel-edge core.

theorem Bananas.core_connected {g : ℕ} (B : Banana g) : B.core.Connected

The two-vertex core underlying every banana is connected.

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

Every positive-length banana graph is connected.

theorem Bananas.core_twoEdgeConnected {g : ℕ} (hg : 1 ≤ g) (B : Banana g) : B.core.TwoEdgeConnected

With at least two strands, the parallel-edge core has no one-edge cut.

theorem Bananas.graph_twoEdgeCutCondition {g : ℕ} (hg : 1 ≤ g) (B : Banana g) : Utilities.TwoEdgeCutCondition (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

Thus a nontrivial banana has no bridge in its subdivided graph.

theorem Bananas.not_linearEquiv_one_chip_sub {g : ℕ} (hg : 1 ≤ g) (B : Banana g) {p q : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V} (hpq : p ≠ q) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip q - oneChip p) 0

Distinct vertices of a nontrivial banana represent distinct degree-one divisor classes.

theorem Bananas.marks_not_linearEquiv {g : ℕ} (hg : 1 ≤ g) (B : Banana g) {u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V} (huv : u ≠ v) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip u - oneChip v) 0

Convenient orientation of degree-one rigidity for an ordered marked pair.

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

The subdivision model has the advertised genus.

theorem Bananas.canonical_divisor_eq_endpoints {g : ℕ} (B : Banana g) : canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B) = (↑g - 1) • (oneChip (leftEndpoint B) + oneChip (rightEndpoint B))

The canonical divisor of a genus-g banana is supported at its two multivalent endpoints, with coefficient g - 1 at each endpoint. The coefficient is an integer, so this also correctly covers the genus-zero single-strand case.