Chip-firing graph isomorphisms

This module transports divisor theory along an equivalence of vertex types that preserves every edge multiplicity. The definition deliberately ignores the orientation chosen for pairs in the raw edge multiset: numEdges is the mathematical graph structure used by chip firing.

structure Utilities.CFGraphIso (G : CFGraph) (H : CFGraph) : Type (max u v)

An isomorphism of chip-firing graphs is an equivalence of their vertex types preserving every edge multiplicity.

• vertexEquiv : G.V ≃ H.V

  The vertex bijection that preserves every edge multiplicity.

• map_num_edges (x y : G.V) : numEdges H (self.vertexEquiv x) (self.vertexEquiv y) = numEdges G x y

def Utilities.CFGraphIso.refl (G : CFGraph) : CFGraphIso G G

The identity graph isomorphism.

Equations

• Utilities.CFGraphIso.refl G = { vertexEquiv := Equiv.refl G.V, map_num_edges := ⋯ }

def Utilities.CFGraphIso.symm {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : CFGraphIso H G

The inverse of a graph isomorphism.

Equations

• φ.symm = { vertexEquiv := φ.vertexEquiv.symm, map_num_edges := ⋯ }

def Utilities.CFGraphIso.trans {G : CFGraph} {H : CFGraph} {K : CFGraph} (φ : CFGraphIso G H) (ψ : CFGraphIso H K) : CFGraphIso G K

The composite of graph isomorphisms.

Equations

• φ.trans ψ = { vertexEquiv := φ.vertexEquiv.trans ψ.vertexEquiv, map_num_edges := ⋯ }

def Utilities.CFGraphIso.mapDiv {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : CFDiv G ≃+ CFDiv H

Relabel an integer-valued vertex function along a graph isomorphism. This is used for both divisors and firing scripts.

Equations

• φ.mapDiv = AddEquiv.arrowCongr φ.vertexEquiv (AddEquiv.refl ℤ)

@[reducible, inline]

abbrev Utilities.CFGraphIso.mapScript {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : firingScript G ≃+ firingScript H

Relabeling a firing script is the same additive equivalence as relabeling a divisor.

Equations

• φ.mapScript = φ.mapDiv

@[simp]

theorem Utilities.CFGraphIso.mapDiv_apply {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) (w : H.V) : φ.mapDiv D w = D (φ.vertexEquiv.symm w)

theorem Utilities.CFGraphIso.mapDiv_apply_vertex {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) (v : G.V) : φ.mapDiv D (φ.vertexEquiv v) = D v

@[simp]

theorem Utilities.CFGraphIso.mapDiv_symm {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : φ.symm.mapDiv = φ.mapDiv.symm

@[simp]

theorem Utilities.CFGraphIso.mapDiv_trans {G : CFGraph} {H : CFGraph} {K : CFGraph} (φ : CFGraphIso G H) (ψ : CFGraphIso H K) : (φ.trans ψ).mapDiv = φ.mapDiv.trans ψ.mapDiv

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

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

@[simp]

theorem Utilities.CFGraphIso.mapDiv_one_chip {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (v : G.V) : φ.mapDiv (oneChip v) = oneChip (φ.vertexEquiv v)

Relabeling carries a one-chip divisor to the corresponding vertex.

@[simp]

theorem Utilities.CFGraphIso.vertex_degree_map {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (v : G.V) : vertexDegree H (φ.vertexEquiv v) = vertexDegree G v

Vertex degree is invariant under graph isomorphism.

@[simp]

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

Divisor degree is invariant under relabeling.

@[simp]

theorem Utilities.CFGraphIso.effective_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) : effective (φ.mapDiv D) ↔ effective D

Effectivity is invariant under relabeling.

@[simp]

theorem Utilities.CFGraphIso.mapDiv_prin {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (σ : firingScript G) : φ.mapDiv ((prin G) σ) = (prin H) (φ.mapScript σ)

Principal divisors commute with relabeling.

@[simp]

theorem Utilities.CFGraphIso.mem_principal_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) : φ.mapDiv D ∈ principalDivisors H ↔ D ∈ principalDivisors G

Membership in the subgroup of principal divisors is invariant under relabeling.

@[simp]

theorem Utilities.CFGraphIso.linear_equiv_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D E : CFDiv G) : linearEquiv H (φ.mapDiv D) (φ.mapDiv E) ↔ linearEquiv G D E

Linear equivalence is invariant under relabeling.

@[simp]

theorem Utilities.CFGraphIso.winnable_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) : winnable H (φ.mapDiv D) ↔ winnable G D

Winnability is invariant under relabeling.

@[simp]

theorem Utilities.CFGraphIso.mem_eff_of_degree_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (E : CFDiv G) (k : ℤ) : φ.mapDiv E ∈ effOfDegree H k ↔ E ∈ effOfDegree G k

Relabeling preserves the set of effective divisors of each degree.

@[simp]

theorem Utilities.CFGraphIso.rank_geq_mapDiv_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (D : CFDiv G) (k : ℤ) : rankGeq H (φ.mapDiv D) k ↔ rankGeq G D k

Every rank lower bound is invariant under relabeling.

@[simp]

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

Baker--Norine rank is invariant under relabeling.

theorem Utilities.CFGraphIso.vertex_card_eq {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : Fintype.card H.V = Fintype.card G.V

Isomorphic graphs have the same number of vertices.

theorem Utilities.CFGraphIso.edge_card_eq {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : H.edges.card = G.edges.card

The raw edge multisets of isomorphic graphs have the same cardinality, even though their choices of pair orientation need not agree.

theorem Utilities.CFGraphIso.genus_eq {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : H.genus = G.genus

Graph genus is invariant under isomorphism.

theorem Utilities.CFGraphIso.graph_connected_map {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (hConnected : graphConnected G) : graphConnected H

Connectivity is transported in the forward direction by a graph isomorphism.

theorem Utilities.CFGraphIso.graph_connected_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : graphConnected H ↔ graphConnected G

Graph connectivity is invariant under isomorphism.

theorem Utilities.CFGraphIso.BNExists_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (r d : ℤ) : BNExists H r d ↔ BNExists G r d

Brill--Noether existence is invariant under graph isomorphism.