Transmission and chip-firing graph isomorphisms

The transmission condition is equivariant for relabelings of a chip-firing graph. In particular, the affine permutation is not changed: an isomorphism only transports the two marked vertices and the witness divisor.

theorem Utilities.CFGraphIso.mapDiv_add_marked_twist {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) (u v : G.V) (a b : ℤ) : φ.mapDiv (D + a • oneChip u - b • oneChip v) = φ.mapDiv D + a • oneChip (φ.vertexEquiv u) - b • oneChip (φ.vertexEquiv v)

Relabeling commutes with every twice-marked divisor twist.

@[simp]

theorem Utilities.CFGraphIso.transmissionInequality_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (a b : ℤ) : TransmissionInequality H (φ.vertexEquiv u) (φ.vertexEquiv v) τ (φ.mapDiv D) a b ↔ TransmissionInequality G u v τ D a b

A single transmission rank inequality is invariant under relabeling the graph, the two marks, and the divisor.

@[simp]

theorem Utilities.CFGraphIso.satisfiesTransmissionOn_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (S : Set (ℤ × ℤ)) : SatisfiesTransmissionOn H (φ.vertexEquiv u) (φ.vertexEquiv v) τ (φ.mapDiv D) S ↔ SatisfiesTransmissionOn G u v τ D S

Restricted transmission tests are invariant under graph relabeling.

@[simp]

theorem Utilities.CFGraphIso.satisfiesTransmission_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) (D : CFDiv G) : SatisfiesTransmission H (φ.vertexEquiv u) (φ.vertexEquiv v) τ (φ.mapDiv D) ↔ SatisfiesTransmission G u v τ D

The complete transmission condition is invariant under graph relabeling.

theorem Utilities.CFGraphIso.satisfiesTransmission_mapDiv {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (h : SatisfiesTransmission G u v τ D) : SatisfiesTransmission H (φ.vertexEquiv u) (φ.vertexEquiv v) τ (φ.mapDiv D)

A transmission witness transports forward along a chip-firing graph isomorphism.

@[simp]

theorem Utilities.CFGraphIso.transmissionExists_map_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) : TransmissionExists H (φ.vertexEquiv u) (φ.vertexEquiv v) τ ↔ TransmissionExists G u v τ

Transmission existence is invariant under graph relabeling.

theorem Utilities.CFGraphIso.transmissionExists_map {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u v : G.V) (τ : AspPerm) (h : TransmissionExists G u v τ) : TransmissionExists H (φ.vertexEquiv u) (φ.vertexEquiv v) τ

Forward form of transmissionExists_map_iff.

Once-marked consequences

theorem Utilities.CFGraphIso.onceMarkedBNExists_map {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u : G.V) (lambda : YoungDiagram) (h : OnceMarkedBNExists G u lambda) : OnceMarkedBNExists H (φ.vertexEquiv u) lambda

A normalized once-marked partition witness transports forward under a graph relabeling.

@[simp]

theorem Utilities.CFGraphIso.onceMarkedBNExists_map_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u : G.V) (lambda : YoungDiagram) : OnceMarkedBNExists H (φ.vertexEquiv u) lambda ↔ OnceMarkedBNExists G u lambda

Once-marked partition occurrence is invariant under relabeling the graph and its marked vertex.

@[simp]

theorem Utilities.CFGraphIso.onceMarkedBNExistence_map_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (u : G.V) : OnceMarkedBNExistence H (φ.vertexEquiv u) ↔ OnceMarkedBNExistence G u

The full once-marked existence predicate is invariant under graph relabeling.