Compatibility between graph and Laplacian equivalences

The graph-isomorphism and certificate layers use the same vertex-equivalence and edge-multiplicity data. This module gives the two presentations explicit conversions, so results from either layer can be used without rebuilding that data by hand.

def Utilities.CFGraphIso.toLaplacianEquiv {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : Certificate.LaplacianEquiv G H

Regard a chip-firing graph isomorphism as a Laplacian-preserving vertex equivalence.

Equations

• φ.toLaplacianEquiv = { toEquiv := φ.vertexEquiv, num_edges_eq := ⋯ }

@[simp]

theorem Utilities.CFGraphIso.toLaplacianEquiv_mapDiv {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) : φ.toLaplacianEquiv.mapDiv D = φ.mapDiv D

@[simp]

theorem Utilities.CFGraphIso.toLaplacianEquiv_mapScript {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (script : firingScript G) : φ.toLaplacianEquiv.mapScript script = φ.mapScript script

def Utilities.Certificate.LaplacianEquiv.toGraphIso {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : CFGraphIso G H

Regard a Laplacian-preserving vertex equivalence as a chip-firing graph isomorphism.

Equations

• equivalence.toGraphIso = { vertexEquiv := equivalence.toEquiv, map_num_edges := ⋯ }

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.toGraphIso_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : equivalence.toGraphIso.mapDiv D = equivalence.mapDiv D

theorem Utilities.Certificate.LaplacianEquiv.toGraphIso_mapScript {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (script : firingScript G) : equivalence.toGraphIso.mapScript script = equivalence.mapScript script

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.toGraphIso_toLaplacianEquiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : equivalence.toGraphIso.toLaplacianEquiv = equivalence

theorem Utilities.Certificate.LaplacianEquiv.transmissionExistence_map_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (x y : G.V) : TransmissionExistence H (equivalence.toEquiv x) (equivalence.toEquiv y) ↔ TransmissionExistence G x y

Full finite-length transmission existence is invariant under Laplacian equivalences. This exposes the graph-isomorphism theorem directly at the certificate API, so relabelings need not reconstruct a second transport object.

@[simp]

theorem Utilities.CFGraphIso.toLaplacianEquiv_toGraphIso {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : φ.toLaplacianEquiv.toGraphIso = φ