Euler accounting for topological graph contractions

GraphContractionCertificate.Valid fixes precisely the edges joining different vertex fibres. This file packages the resulting Euler accounting. It is intentionally phrased using directed multiplicities, because that is the representation-independent quantity supplied by numEdges.

In particular, an equal-genus valid contraction has exactly the amount of internal directed multiplicity forced by its loss of vertices. Together with connected fibres, the remaining graph-theoretic input for saying that every fibre is a tree is the usual connected-graph lower bound on its internal edge count. Keeping this boundary explicit avoids silently treating arbitrary quotients as rank-preserving contractions.

def Utilities.Certificate.GraphContractionCertificate.internalDirectedMultiplicity {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : ℤ

The total directed multiplicity of source edges which stay inside one vertex fibre.

Equations

• c.internalDirectedMultiplicity = ∑ x : G.V, ∑ y : G.V, if c.vertexMap x = c.vertexMap y then ↑(numEdges G x y) else 0

def Utilities.Certificate.GraphContractionCertificate.externalDirectedMultiplicity {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : ℤ

The total directed multiplicity of source edges which join two distinct vertex fibres.

Equations

• c.externalDirectedMultiplicity = ∑ x : G.V, ∑ y : G.V, if c.vertexMap x ≠ c.vertexMap y then ↑(numEdges G x y) else 0

def Utilities.Certificate.GraphContractionCertificate.fibreVertices {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (target : H.V) : Finset G.V

The vertices in one contraction fibre.

Equations

• c.fibreVertices target = {x : G.V | c.vertexMap x = target}

theorem Utilities.Certificate.GraphContractionCertificate.fibreVertices_nonempty {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (target : H.V) : (c.fibreVertices target).Nonempty

noncomputable def Utilities.Certificate.GraphContractionCertificate.fibreGraph {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (target : H.V) : CFGraph

The actual induced graph carried by a contraction fibre.

Equations

• c.fibreGraph hValid target = Utilities.inducedSubgraph G (c.fibreVertices target) ⋯

theorem Utilities.Certificate.GraphContractionCertificate.inducedFibre_connected {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (hFibres : c.ConnectedFibres) (target : H.V) : _root_.graphConnected (inducedSubgraph G (c.fibreVertices target) ⋯)

The finite-cut connected-fibre condition is precisely enough to make each induced fibre graph connected.

theorem Utilities.Certificate.GraphContractionCertificate.fibreGraph_connected {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (hFibres : c.ConnectedFibres) (target : H.V) : _root_.graphConnected (c.fibreGraph hValid target)

theorem Utilities.Certificate.GraphContractionCertificate.fibreGraph_connected_of_topologicalValid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hTopological : c.TopologicalValid) (target : H.V) : _root_.graphConnected (c.fibreGraph ⋯ target)

Convenience form of fibre connectedness for a topological contraction.

theorem Utilities.Certificate.GraphContractionCertificate.internal_add_external_eq_total {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.internalDirectedMultiplicity + c.externalDirectedMultiplicity = ∑ x : G.V, vertexDegree G x

The source directed multiplicity partitions into internal and external fibre contributions.

theorem Utilities.Certificate.GraphContractionCertificate.externalDirectedMultiplicity_eq_degreeSum {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) : c.externalDirectedMultiplicity = ∑ a : H.V, vertexDegree H a

The off-fibre directed multiplicity is exactly the degree sum of the quotient graph.

theorem Utilities.Certificate.GraphContractionCertificate.internalDirectedMultiplicity_eq_two_mul_edgeLoss {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) : c.internalDirectedMultiplicity = 2 * (↑G.edges.card - ↑H.edges.card)

Euler accounting in directed form. The contracted internal multiplicity is twice the loss of edge occurrences.

theorem Utilities.Certificate.GraphContractionCertificate.internalDirectedMultiplicity_eq_two_mul_vertexLoss_of_genus_eq {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (hGenus : G.genus = H.genus) : c.internalDirectedMultiplicity = 2 * (↑(Fintype.card G.V) - ↑(Fintype.card H.V))

If a valid contraction has equal cyclomatic genus, its internal directed multiplicity is exactly twice the number of vertices removed. This is the Euler identity underlying the assertion that connected fibres must be trees.