Regular rotation maps of simple graphs

Reingold's algorithm for undirected connectivity Reingold, Section 4 Arora and Barak, Section 21.4 works on regular graphs of a fixed degree, so it first turns the input graph into one, without changing which vertices are connected. Each vertex v of a simple graph G on V is replaced by a cycle of slots (v, w), one for each w : V, the end at v of a potential edge {v, w}. The slots of v are joined in the cyclic order of a permutation σ of V with a single cycle (such as finRotate n on Fin n), and the slot (v, w) is joined to the slot (w, v) when v and w are adjacent, and carries a self-loop otherwise. The result, Cslib.RotationMap.slotGraph G σ, is a 3-regular multigraph on V × V, and (w, b) is reachable from (v, a) exactly when w is reachable from v in G (reachable_slotGraph_iff).

To reach a prescribed label type B, the labels are extended along an embedding D ↪ B; the new labels carry self-loops (Cslib.RotationMap.extendLabels). This keeps the simple graph of the rotation map (toSimpleGraph_extendLabels), and when B has at least twice as many elements as D, at least half of the edges at every vertex are self-loops (card_le_two_mul_card_filter_neighbor_extendLabels_eq), which is what makes connected components spectral expanders (Cslib.RotationMap.spectralExpansion_le_of_preconnected).

Main definitions

• Cslib.RotationMap.decodeLabel: the partial inverse of an embedding of labels.
• Cslib.RotationMap.extendLabels: extend the labels of a rotation map by self-loops.
• Cslib.RotationMap.slotSwap: the involution of the slots exchanging the two ends of an edge.
• Cslib.RotationMap.SlotLabel, Cslib.RotationMap.slotGraph: the 3-regular slot graph of a simple graph and its labels.

Main results

• Cslib.RotationMap.toSimpleGraph_extendLabels: extending the labels does not change the simple graph.
• Cslib.RotationMap.card_le_two_mul_card_filter_neighbor_extendLabels_eq: enough new labels make at least half of the edges self-loops.
• Cslib.RotationMap.reachable_slotGraph_iff: the slot graph has the connectivity of the simple graph.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.RotationMap.decodeLabel {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (enc : D ↪ B) (b : B) : Option D

The label of D that enc maps to b, if there is one, by Mathlib's computable inverse Function.Embedding.invOfMemRange on the range of enc.

theorem Cslib.RotationMap.decodeLabel_eq_some_iff {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (enc : D ↪ B) {b : B} {i : D} : decodeLabel enc b = some i ↔ enc i = b

decodeLabel enc is the partial inverse of enc.

@[simp]

theorem Cslib.RotationMap.decodeLabel_apply {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (enc : D ↪ B) (i : D) : decodeLabel enc (enc i) = some i

decodeLabel enc recovers the labels of D.

theorem Cslib.RotationMap.decodeLabel_eq_none_iff {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (enc : D ↪ B) {b : B} : decodeLabel enc b = none ↔ ∀ (i : D), enc i ≠ b

decodeLabel enc b is none exactly when b is not a label of D.

def Cslib.RotationMap.extendLabels {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) : RotationMap V B

G with its labels extended along an embedding enc : D ↪ B: the label enc i at a vertex is its i-th edge in G, and every label outside the range of enc is a self-loop.

@[simp]

theorem Cslib.RotationMap.rot_extendLabels_apply {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) (v : V) (i : D) : (G.extendLabels enc).rot (v, enc i) = Prod.map id (⇑enc) (G.rot (v, i))

The label enc i of G.extendLabels enc is the i-th edge of G.

@[simp]

theorem Cslib.RotationMap.neighbor_extendLabels_apply {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) (v : V) (i : D) : (G.extendLabels enc).neighbor v (enc i) = G.neighbor v i

The enc i-th neighbor in G.extendLabels enc is the i-th neighbor in G.

theorem Cslib.RotationMap.rot_extendLabels_of_forall_ne {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) (v : V) {b : B} (hb : ∀ (i : D), enc i ≠ b) : (G.extendLabels enc).rot (v, b) = (v, b)

A label outside the range of enc is a self-loop of G.extendLabels enc.

theorem Cslib.RotationMap.neighbor_extendLabels_of_forall_ne {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) (v : V) {b : B} (hb : ∀ (i : D), enc i ≠ b) : (G.extendLabels enc).neighbor v b = v

A label outside the range of enc is a self-loop of G.extendLabels enc.

@[simp]

theorem Cslib.RotationMap.toSimpleGraph_extendLabels {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) : (G.extendLabels enc).toSimpleGraph = G.toSimpleGraph

Extending the labels does not change the simple graph: the new edges are self-loops.

theorem Cslib.RotationMap.card_le_two_mul_card_filter_neighbor_extendLabels_eq {V : Type u_1} {D : Type u_2} {B : Type u_3} [Fintype D] [DecidableEq B] (G : RotationMap V D) (enc : D ↪ B) [Fintype B] [DecidableEq V] (hB : 2 * Fintype.card D ≤ Fintype.card B) (v : V) : Fintype.card B ≤ 2 * {b : B | (G.extendLabels enc).neighbor v b = v}.card

If B has at least twice as many elements as D, at least half of the edges at every vertex of G.extendLabels enc are self-loops.

def Cslib.RotationMap.slotSwap {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (p : V × V) : V × V

The involution of the slots V × V of a simple graph G: the slot (v, w) is exchanged with (w, v) when v and w are adjacent, and fixed otherwise.

theorem Cslib.RotationMap.slotSwap_involutive {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : Function.Involutive (slotSwap G)

Exchanging the ends of an edge twice gives back the slot.

@[reducible, inline]

abbrev Cslib.RotationMap.SlotLabel : Type

The three labels of the slot graph: inl () for the edge of G at a slot, and inr ((), (), false) and inr ((), (), true) for the cycle of the slots of a vertex, forwards and backwards.

def Cslib.RotationMap.slotGraph {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) : RotationMap (V × V) SlotLabel

The slot graph of a simple graph G on V, a 3-regular multigraph on the slots V × V Reingold, Section 4: the edge inl () at (v, w) leads to (w, v) if v and w are adjacent and is a self-loop otherwise, and the edges inr ((), (), false) and inr ((), (), true) lead to (v, σ w) and (v, σ⁻¹ w), so that the slots of each vertex form the cycles of σ.

@[simp]

theorem Cslib.RotationMap.rot_slotGraph_inl {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).rot (p, Sum.inl ()) = (slotSwap G p, Sum.inl ())

The edge inl () of slotGraph G σ exchanges the two ends of an edge of G.

@[simp]

theorem Cslib.RotationMap.rot_slotGraph_inr_false {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).rot (p, Sum.inr ((), (), false)) = ((p.1, σ p.2), Sum.inr ((), (), true))

The edge inr ((), (), false) of slotGraph G σ at (v, w) leads to (v, σ w) and returns along inr ((), (), true).

@[simp]

theorem Cslib.RotationMap.rot_slotGraph_inr_true {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).rot (p, Sum.inr ((), (), true)) = ((p.1, (Equiv.symm σ) p.2), Sum.inr ((), (), false))

The edge inr ((), (), true) of slotGraph G σ at (v, w) leads to (v, σ⁻¹ w) and returns along inr ((), (), false).

@[simp]

theorem Cslib.RotationMap.neighbor_slotGraph_inl {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).neighbor p (Sum.inl ()) = slotSwap G p

The edge inl () exchanges the two ends of an edge of G.

@[simp]

theorem Cslib.RotationMap.neighbor_slotGraph_inr_false {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).neighbor p (Sum.inr ((), (), false)) = (p.1, σ p.2)

The edge inr ((), (), false) at (v, w) leads to (v, σ w).

@[simp]

theorem Cslib.RotationMap.neighbor_slotGraph_inr_true {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (p : V × V) : (slotGraph G σ).neighbor p (Sum.inr ((), (), true)) = (p.1, (Equiv.symm σ) p.2)

The edge inr ((), (), true) at (v, w) leads to (v, σ⁻¹ w).

theorem Cslib.RotationMap.card_slotLabel : Fintype.card SlotLabel = 3

The slot graph has three labels.

theorem Cslib.RotationMap.reachable_fst_of_reachable_slotGraph {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) {p q : V × V} (h : (slotGraph G σ).toSimpleGraph.Reachable p q) : G.Reachable p.1 q.1

Every edge of the slot graph stays at a vertex of G or follows an edge of G.

theorem Cslib.RotationMap.reachable_slotGraph_iff {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (hσ : ∀ (a b : V), σ.SameCycle a b) {v w a b : V} : (slotGraph G σ).toSimpleGraph.Reachable (v, a) (w, b) ↔ G.Reachable v w

The slot graph has the connectivity of the simple graph: if σ has a single cycle, the slot (w, b) is reachable from (v, a) exactly when w is reachable from v in G.