Rotation maps of simple graphs

A rotation map determines a simple graph, in which distinct vertices are adjacent when an edge joins them (RotationMap.toSimpleGraph). When the rotation map has neither self-loops nor parallel edges (RotationMap.IsSimple), this loses nothing: the simple graph is regular of degree |D|, its walk operator averages over the neighbors in the simple graph, and its edges between two sets of vertices are those of the rotation map (IsSimple.card_interedges), so the results on rotation maps, such as the expander mixing lemma, apply to it. Conversely, every d-regular simple graph has a simple rotation map with labels Fin d (exists_isSimple_toSimpleGraph_eq).

Main definitions

• Cslib.RotationMap.toSimpleGraph: the simple graph underlying a rotation map.
• Cslib.RotationMap.IsSimple: a rotation map without self-loops or parallel edges.

Main results

• Cslib.RotationMap.IsSimple.isRegularOfDegree: the simple graph of a simple rotation map with labels D is regular of degree |D|.
• Cslib.RotationMap.IsSimple.walk_apply_eq_sum_neighborFinset: its walk operator averages over the neighbors.
• Cslib.RotationMap.IsSimple.card_interedges: its edges between two sets of vertices are those of the rotation map.
• Cslib.RotationMap.exists_isSimple_toSimpleGraph_eq: every d-regular simple graph is presented by a simple rotation map with labels Fin d.

References

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

def Cslib.RotationMap.toSimpleGraph {V : Type u_1} {D : Type u_2} (G : RotationMap V D) : SimpleGraph V

The simple graph underlying G: distinct vertices are adjacent when an edge of G joins them. Self-loops are dropped and parallel edges merged.

@[simp]

theorem Cslib.RotationMap.toSimpleGraph_adj {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {u v : V} : G.toSimpleGraph.Adj u v ↔ u ≠ v ∧ ∃ (i : D), G.neighbor u i = v

Distinct vertices are adjacent in the simple graph of G when an edge of G joins them.

@[instance_reducible]

instance Cslib.RotationMap.instDecidableRelAdjToSimpleGraphOfDecidableEqOfFintype {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] : DecidableRel G.toSimpleGraph.Adj

Adjacency in the simple graph of a rotation map with finitely many labels is decidable.

structure Cslib.RotationMap.IsSimple {V : Type u_1} {D : Type u_2} (G : RotationMap V D) : Prop

G is simple: it has no self-loops and no parallel edges.

• neighbor_ne (v : V) (i : D) : G.neighbor v i ≠ v

  No edge joins a vertex to itself.

• neighbor_injective (v : V) : Function.Injective (G.neighbor v)

  No two edges at a vertex lead to the same neighbor.

theorem Cslib.RotationMap.IsSimple.toSimpleGraph_adj_iff {V : Type u_1} {D : Type u_2} {G : RotationMap V D} (hG : G.IsSimple) {u v : V} : G.toSimpleGraph.Adj u v ↔ ∃ (i : D), G.neighbor u i = v

In the simple graph of a simple rotation map, u and v are adjacent exactly when v is a neighbor of u.

theorem Cslib.RotationMap.IsSimple.neighborFinset_eq {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype D] [DecidableEq V] (hG : G.IsSimple) (v : V) [Fintype ↑(G.toSimpleGraph.neighborSet v)] : G.toSimpleGraph.neighborFinset v = Finset.image (G.neighbor v) Finset.univ

The neighbors of v in the simple graph are the ends of the edges at v.

theorem Cslib.RotationMap.IsSimple.isRegularOfDegree {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype D] (hG : G.IsSimple) [G.toSimpleGraph.LocallyFinite] : G.toSimpleGraph.IsRegularOfDegree (Fintype.card D)

The simple graph of a simple rotation map with labels D is regular of degree |D|.

theorem Cslib.RotationMap.IsSimple.walk_apply_eq_sum_neighborFinset {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype D] (hG : G.IsSimple) [G.toSimpleGraph.LocallyFinite] (f : V → ℝ) (v : V) : G.walk f v = (∑ w ∈ G.toSimpleGraph.neighborFinset v, f w) / ↑(Fintype.card D)

The walk operator of a simple rotation map averages over the neighbors in its simple graph.

theorem Cslib.RotationMap.IsSimple.card_interedges {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype D] [DecidableEq V] [DecidableRel G.toSimpleGraph.Adj] (hG : G.IsSimple) (S T : Finset V) : (G.toSimpleGraph.interedges S T).card = (G.interedges S T).card

The edges of the simple graph between two sets of vertices are those of the rotation map.

theorem Cslib.RotationMap.exists_isSimple_toSimpleGraph_eq {V : Type u_1} {H : SimpleGraph V} [H.LocallyFinite] {d : ℕ} (hH : H.IsRegularOfDegree d) : ∃ (G : RotationMap V (Fin d)), G.IsSimple ∧ G.toSimpleGraph = H

Every d-regular simple graph is the simple graph of a simple rotation map with labels Fin d, obtained by numbering the neighbors of each vertex Arora and Barak, Section 21.3.