Tree fibres in equal-genus topological contractions

The first ingredient is a small general fact about finite loopless multigraphs: a connected graph has at least one fewer edge occurrence than vertices. We prove it by forgetting multiplicities, taking a spanning tree in the resulting simple graph, and observing that every simple edge has an ambient occurrence.

This is the local inequality used with the Euler accounting in GraphContractionEuler: after the still-to-be-packaged partition identity for the fibre edge multisets, equality of source and target genus forces equality in this bound fibre by fibre.

theorem Utilities.underlyingSimpleGraph_edgeFinset_card_le (G : CFGraph) : (underlyingSimpleGraph G).edgeFinset.card ≤ G.edges.card

Forgetting multiplicities cannot create more edges than the ambient multigraph has occurrences.

theorem Utilities.graph_connected_card_vertices_le_card_edges_add_one (G : CFGraph) (hConnected : graphConnected G) : Fintype.card G.V ≤ G.edges.card + 1

Every connected loopless multigraph has at least |V|-1 edge occurrences. Parallel edges are allowed.

theorem Utilities.genus_nonneg_of_graph_connected (G : CFGraph) (hConnected : graphConnected G) : 0 ≤ G.genus

The cyclomatic genus of a connected loopless multigraph is nonnegative.

theorem Utilities.Certificate.GraphContractionCertificate.sum_fibreVertices_card {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : ∑ target : H.V, (c.fibreVertices target).card = Fintype.card G.V

The fibre vertex cards partition the source vertex set.

theorem Utilities.Certificate.GraphContractionCertificate.sum_fibreGraph_edge_cards {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) : ∑ target : H.V, (c.fibreGraph hValid target).edges.card = (Multiset.filter (fun (edge : G.V × G.V) => c.vertexMap edge.1 = c.vertexMap edge.2) G.edges).card

Fibre edge cards partition the source edge occurrences which are contracted by the vertex map.

theorem Utilities.Certificate.GraphContractionCertificate.internalDirectedMultiplicity_eq_two_mul_contractedEdgeCard {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.internalDirectedMultiplicity = 2 * ↑(Multiset.filter (fun (edge : G.V × G.V) => c.vertexMap edge.1 = c.vertexMap edge.2) G.edges).card

Internal directed multiplicity counts every contracted edge occurrence at each of its two endpoints.

theorem Utilities.Certificate.GraphContractionCertificate.internalDirectedMultiplicity_eq_two_mul_sum_fibreGraph_edge_cards {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) : c.internalDirectedMultiplicity = 2 * ∑ target : H.V, ↑(c.fibreGraph hValid target).edges.card

The internal directed multiplicity is twice the total number of edge occurrences in the induced fibre graphs.

theorem Utilities.Certificate.GraphContractionCertificate.genus_le_of_topologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) : H.genus ≤ G.genus

A connected-fibre quotient cannot increase cyclomatic genus.

theorem Utilities.Certificate.GraphContractionCertificate.fibreGraph_edge_card_add_one_eq_vertex_card_of_genus_eq {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (hGenus : G.genus = H.genus) (target : H.V) : (c.fibreGraph ⋯ target).edges.card + 1 = Fintype.card (c.fibreGraph ⋯ target).V

If a connected-fibre quotient preserves genus, every fibre has exactly one fewer edge occurrence than vertices.

theorem Utilities.Certificate.GraphContractionCertificate.fibreGraph_underlyingSimpleGraph_isTree_of_genus_eq {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (hGenus : G.genus = H.genus) (target : H.V) : (underlyingSimpleGraph (c.fibreGraph ⋯ target)).IsTree

In an equal-genus topological contraction, each fibre is a tree after forgetting parallel-edge multiplicities.

theorem Utilities.Certificate.GraphContractionCertificate.fibreGraph_genus_nonneg_of_topologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (target : H.V) : 0 ≤ (c.fibreGraph ⋯ target).genus

Each connected contraction fibre has nonnegative cyclomatic genus.