Transport across graph isomorphisms

The recursive upper bound is naturally proved on Cartesian products. To apply those product constructions to hypercubes, we need a lightweight way to move pebbling distributions and solvability statements across graph isomorphisms.

structure PebblingLean.GraphIso {V : Type u} {W : Type v} (G : Graph V) (H : Graph W) : Type (max u v)

An adjacency-preserving equivalence between two simple graphs.

• toEquiv : V ≃ W

  The underlying equivalence between the vertex types.

• adj_iff {x y : V} : G.Adj x y ↔ H.Adj (self.toEquiv x) (self.toEquiv y)

  The equivalence preserves and reflects adjacency.

def PebblingLean.GraphIso.mapDistribution {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} (iso : GraphIso G H) (D : Pebbling V) : Pebbling W

Transport a pebbling distribution across the vertex equivalence.

Equations

• iso.mapDistribution D w = D (iso.toEquiv.symm w)

@[simp]

theorem PebblingLean.GraphIso.mapDistribution_apply {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} (iso : GraphIso G H) (D : Pebbling V) (v : V) : iso.mapDistribution D (iso.toEquiv v) = D v

theorem PebblingLean.GraphIso.size_mapDistribution {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [Fintype V] [Fintype W] (iso : GraphIso G H) (D : Pebbling V) : (iso.mapDistribution D).size = D.size

def PebblingLean.GraphIso.symm {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} (iso : GraphIso G H) : GraphIso H G

Reverse a graph isomorphism.

Equations

• iso.symm = { toEquiv := iso.toEquiv.symm, adj_iff := ⋯ }

theorem PebblingLean.GraphIso.map_move {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [DecidableEq V] [DecidableEq W] (iso : GraphIso G H) {D E : Pebbling V} (hmove : Pebbling.Move G D E) : Pebbling.Move H (iso.mapDistribution D) (iso.mapDistribution E)

theorem PebblingLean.GraphIso.map_reaches {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [DecidableEq V] [DecidableEq W] (iso : GraphIso G H) {D E : Pebbling V} (hreach : Pebbling.Reaches G D E) : Pebbling.Reaches H (iso.mapDistribution D) (iso.mapDistribution E)

theorem PebblingLean.GraphIso.map_canReachAtLeast {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [DecidableEq V] [DecidableEq W] (iso : GraphIso G H) {D : Pebbling V} {target : W} {T : ℕ} (hcan : Pebbling.CanReachAtLeast G D (iso.toEquiv.symm target) T) : Pebbling.CanReachAtLeast H (iso.mapDistribution D) target T

theorem PebblingLean.GraphIso.map_solvableAtLeast {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [DecidableEq V] [DecidableEq W] (iso : GraphIso G H) {D : Pebbling V} {T : ℕ} (hsolv : Pebbling.SolvableAtLeast G D T) : Pebbling.SolvableAtLeast H (iso.mapDistribution D) T

theorem PebblingLean.GraphIso.map_minOccupiedPileSize {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} (iso : GraphIso G H) {D : Pebbling V} {S : ℕ} (hmin : D.MinOccupiedPileSize S) : (iso.mapDistribution D).MinOccupiedPileSize S

theorem PebblingLean.GraphIso.map_hasSolvableAtMostSize {V : Type u} {W : Type v} {G : Graph V} {H : Graph W} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (iso : GraphIso G H) {T k : ℕ} (h : Pebbling.HasSolvableAtMostSize G T k) : Pebbling.HasSolvableAtMostSize H T k