Reindexing the vertices of a rotation map

An explicit equivalence transports a graph to a new vertex representation, preserving its edge labels and spectral expansion. In particular, a computable numbering turns a graph on structured vertices into an indexed graph without choosing an enumeration.

Main definitions

• Cslib.RotationMap.reindex: transport the vertex representation along an equivalence.
• Cslib.RotationMap.reindexRot: the functional transport program.

Main results

• Cslib.RotationMap.rot_reindex: the rotation map of a reindexed graph.
• Cslib.RotationMap.walk_reindex: the walk operator transforms by composition.
• Cslib.RotationMap.spectralExpansion_reindex: spectral expansion is unchanged.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 21

def Cslib.RotationMap.reindexRot {V : Type u_1} {W : Type u_2} {D : Type u_3} (forward : V → W) (backward : W → V) (rotate : V × D → V × D) (p : W × D) : W × D

Decode a renamed vertex, rotate, and encode the resulting vertex, retaining the edge label.

def Cslib.RotationMap.reindex {V : Type u_1} {W : Type u_2} {D : Type u_3} (G : RotationMap V D) (e : V ≃ W) : RotationMap W D

Rename the vertices of a graph, retaining every outgoing and return edge label.

@[simp]

theorem Cslib.RotationMap.rot_reindex {V : Type u_1} {W : Type u_2} {D : Type u_3} (G : RotationMap V D) (e : V ≃ W) (p : W × D) : (G.reindex e).rot p = (e (G.rot (e.symm p.1, p.2)).1, (G.rot (e.symm p.1, p.2)).2)

The rotation map of a reindexed graph decodes the vertex, rotates in G, and re-encodes the resulting vertex.

@[simp]

theorem Cslib.RotationMap.neighbor_reindex {V : Type u_1} {W : Type u_2} {D : Type u_3} (G : RotationMap V D) (e : V ≃ W) (w : W) (d : D) : (G.reindex e).neighbor w d = e (G.neighbor (e.symm w) d)

The neighbor after renaming vertices is the renamed original neighbor.

theorem Cslib.RotationMap.walk_reindex {V : Type u_1} {W : Type u_2} {D : Type u_3} [Fintype D] (G : RotationMap V D) (e : V ≃ W) (f : W → ℝ) (w : W) : (G.reindex e).walk f w = G.walk (f ∘ ⇑e) (e.symm w)

The walk on renamed vertices composes with the equivalence and its inverse.

@[simp]

theorem Cslib.RotationMap.spectralExpansion_reindex {V : Type u_1} {W : Type u_2} {D : Type u_3} [Fintype V] [Fintype W] [Fintype D] (G : RotationMap V D) (e : V ≃ W) : (G.reindex e).spectralExpansion = G.spectralExpansion

Explicit vertex renaming preserves spectral expansion, including empty vertex types.