Topology and gonality of the fossil

The short library name fossil means the degree-one Abel--Jacobi image, or 2-edge-connectivization, of a connected graph. This file packages the facts needed by public applications: the fossil remains connected, has the same cyclomatic genus and divisorial gonality, and has no one-edge cuts or leaves.

theorem Utilities.graph_connected_fossil (G : CFGraph) (hConnected : graphConnected G) : graphConnected (fossil G)

A connected graph has a connected fossil.

theorem Utilities.genus_fossil (G : CFGraph) (hConnected : graphConnected G) : (fossil G).genus = G.genus

The fossil has the same cyclomatic genus as a connected graph.

The proof avoids a separate edge-count analysis of the bridge forest. Take a divisor in the nonspecial range for both graphs. Fossil pushforward preserves its degree and rank, while Riemann--Roch says that this rank is degree - genus on each side, forcing the genera to agree.

theorem Utilities.twoEdgeCutCondition_fossil (G : CFGraph) (hConnected : graphConnected G) : TwoEdgeCutCondition (fossil G)

A connected fossil has no one-edge cut. If a proper cut had total multiplicity one, its unique crossing occurrence would define a SeparatingEdgeCut; its endpoints would then be equivalent one-chip classes, contradicting that fossil vertices are already those classes.

theorem Utilities.fossil_vertex_degree_ne_one (G : CFGraph) (hConnected : graphConnected G) (q : (fossil G).V) : vertexDegree (fossil G) q ≠ 1

In particular, a connected fossil has no degree-one vertices.

theorem Utilities.divisorialGonality_fossil (G : CFGraph) (hConnected : graphConnected G) : Gonality.divisorialGonality (fossil G) = Gonality.divisorialGonality G

Divisorial gonality is unchanged by passage to the fossil.