Homomorphisms and restrictions of rotation maps

A homomorphism φ : G.Hom G' between two rotation maps with the same labels is a map of the vertices under which the rotation map of G' follows that of G, label by label: the i-th edge at φ v in G' is the image of the i-th edge at v in G, and it arrives with the same label. So φ maps the walk of G from v along any labels to the walk of G' from φ v along the same labels (Cslib.RotationMap.Hom.neighbor_pow_map): the walks of G' from φ v are exactly the images of the walks of G from v, and every vertex reachable from φ v is the image of a vertex reachable from v (Cslib.RotationMap.Hom.exists_reachable_apply_eq). Homomorphisms are compatible with powers, relabelling and zig-zag products, so a graph product of an image is the image of the product.

The basic example is the restriction G.restrict S hS of G to a set S of vertices closed under taking neighbors, such as the set of the vertices reachable from a given vertex (Cslib.RotationMap.componentGraph), with the inclusion G.restrictHom S hS into G. Reingold's algorithm for undirected connectivity Reingold transforms a graph by powers and zig-zag products, and its analysis runs on the connected component of the start vertex: the transform of the component maps into the transform of the graph, so walks in one are walks in the other.

Main definitions

• Cslib.RotationMap.Hom: homomorphisms of rotation maps with the same labels.
• Cslib.RotationMap.Hom.id, Cslib.RotationMap.Hom.comp: the identity homomorphism and the composition of homomorphisms.
• Cslib.RotationMap.Hom.pow, Cslib.RotationMap.Hom.relabel, Cslib.RotationMap.Hom.zigzag: the induced homomorphisms of powers, relabellings and zig-zag products.
• Cslib.RotationMap.restrict, Cslib.RotationMap.restrictHom: the restriction to a set of vertices closed under taking neighbors, and its inclusion.
• Cslib.RotationMap.componentGraph: the restriction to the vertices reachable from a vertex.
• Cslib.RotationMap.componentHom: the inclusion of that restriction into the graph.

Main results

• Cslib.RotationMap.Hom.neighbor_map, Cslib.RotationMap.Hom.neighbor_pow_map: homomorphisms map neighbors to neighbors and walks to walks along the same labels.
• Cslib.RotationMap.reachable_neighbor: every neighbor of a vertex is reachable from it.
• Cslib.RotationMap.Hom.reachable_map, Cslib.RotationMap.Hom.exists_reachable_apply_eq, Cslib.RotationMap.Hom.reachable_apply_iff: homomorphisms map reachable vertices to reachable vertices, and lift the walks from the image of a vertex.
• Cslib.RotationMap.mem_of_reachable: a set closed under taking neighbors contains every vertex reachable from it.
• Cslib.RotationMap.preconnected_componentGraph: the restriction to the vertices reachable from a vertex is connected.

References

• O. Reingold, Undirected connectivity in log-space
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

structure Cslib.RotationMap.Hom {V : Type u_1} {W : Type u_2} {D : Type u_4} (G : RotationMap V D) (G' : RotationMap W D) : Type (max u_1 u_2)

A homomorphism from G to G', rotation maps with the same labels: a map of the vertices under which the rotation map of G' follows that of G. The i-th edge at φ v in G' is the image of the i-th edge at v in G, and it arrives with the same label.

• toFun : V → W

  The map of the vertices.

• rot_map' (v : V) (i : D) : G'.rot (self.toFun v, i) = Prod.map self.toFun id (G.rot (v, i))

  The rotation map of G' at the image of a dart is the image of the rotation map of G.

@[instance_reducible]

instance Cslib.RotationMap.Hom.instFunLike {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} : FunLike (G.Hom G') V W

A homomorphism of rotation maps coerces to its map of the vertices.

@[simp]

theorem Cslib.RotationMap.Hom.toFun_eq_coe {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') : φ.toFun = ⇑φ

The underlying map of a homomorphism is its coercion to a function.

theorem Cslib.RotationMap.Hom.rot_map {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (v : V) (i : D) : G'.rot (φ v, i) = Prod.map (⇑φ) id (G.rot (v, i))

The rotation map of G' at the image of a dart is the image of the rotation map of G.

theorem Cslib.RotationMap.Hom.neighbor_map {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (v : V) (i : D) : G'.neighbor (φ v) i = φ (G.neighbor v i)

A homomorphism maps the i-th neighbor of v to the i-th neighbor of the image of v.

theorem Cslib.RotationMap.Hom.ext {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} {φ ψ : G.Hom G'} (h : ∀ (v : V), φ v = ψ v) : φ = ψ

Homomorphisms with the same map of the vertices are equal.

theorem Cslib.RotationMap.Hom.ext_iff {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} {φ ψ : G.Hom G'} : φ = ψ ↔ ∀ (v : V), φ v = ψ v

def Cslib.RotationMap.Hom.id {V : Type u_1} {D : Type u_4} (G : RotationMap V D) : G.Hom G

The identity homomorphism.

@[simp]

theorem Cslib.RotationMap.Hom.coe_id {V : Type u_1} {D : Type u_4} (G : RotationMap V D) : ⇑(Hom.id G) = id

The identity homomorphism is the identity map.

theorem Cslib.RotationMap.Hom.id_apply {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (v : V) : (Hom.id G) v = v

The identity homomorphism fixes every vertex.

def Cslib.RotationMap.Hom.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} {G'' : RotationMap X D} (ψ : G'.Hom G'') (φ : G.Hom G') : G.Hom G''

The composition of homomorphisms.

@[simp]

theorem Cslib.RotationMap.Hom.comp_apply {V : Type u_1} {W : Type u_2} {X : Type u_3} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} {G'' : RotationMap X D} (ψ : G'.Hom G'') (φ : G.Hom G') (v : V) : (ψ.comp φ) v = ψ (φ v)

The composition of homomorphisms applies them in turn.

theorem Cslib.RotationMap.Hom.powRot_map {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (t : ℕ) (v : V) (k : Fin t → D) : G'.powRot t (φ v, k) = Prod.map (⇑φ) id (G.powRot t (v, k))

A homomorphism maps walks to walks: the rotation map of the walks of length t follows it.

def Cslib.RotationMap.Hom.pow {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (t : ℕ) : (G.pow t).Hom (G'.pow t)

A homomorphism of rotation maps is a homomorphism of their t-th powers.

@[simp]

theorem Cslib.RotationMap.Hom.pow_apply {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (t : ℕ) (v : V) : (φ.pow t) v = φ v

The homomorphism of the powers is the same map of the vertices.

theorem Cslib.RotationMap.Hom.neighbor_pow_map {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (t : ℕ) (v : V) (k : Fin t → D) : (G'.pow t).neighbor (φ v) k = φ ((G.pow t).neighbor v k)

A homomorphism maps the walk from v along k to the walk from φ v along k.

def Cslib.RotationMap.Hom.relabel {V : Type u_1} {W : Type u_2} {D : Type u_4} {E : Type u_5} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (e : D ≃ E) : (G.relabel e).Hom (G'.relabel e)

A homomorphism of rotation maps is a homomorphism of their relabellings.

@[simp]

theorem Cslib.RotationMap.Hom.relabel_apply {V : Type u_1} {W : Type u_2} {D : Type u_4} {E : Type u_5} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (e : D ≃ E) (v : V) : (φ.relabel e) v = φ v

The homomorphism of the relabellings is the same map of the vertices.

def Cslib.RotationMap.Hom.zigzag {V : Type u_1} {W : Type u_2} {D : Type u_4} {E : Type u_5} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (H : RotationMap D E) : (G.zigzag H).Hom (G'.zigzag H)

A homomorphism of rotation maps with labels D induces a homomorphism of their zig-zag products with a graph H on D, acting on the first coordinate.

@[simp]

theorem Cslib.RotationMap.Hom.zigzag_apply {V : Type u_1} {W : Type u_2} {D : Type u_4} {E : Type u_5} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (H : RotationMap D E) (p : V × D) : (φ.zigzag H) p = (φ p.1, p.2)

The homomorphism of the zig-zag products maps the vertex (v, k) to (φ v, k).

def Cslib.RotationMap.restrict {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (S : Set V) (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) : RotationMap (↑S) D

The restriction of G to a set S of vertices closed under taking neighbors: the rotation map of G on the darts at the vertices of S.

@[simp]

theorem Cslib.RotationMap.rot_restrict {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (S : Set V) (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) (p : ↑S × D) : (G.restrict S hS).rot p = (⟨G.neighbor (↑p.1) p.2, ⋯⟩, (G.rot (↑p.1, p.2)).2)

The rotation map of a restriction of G is the rotation map of G.

def Cslib.RotationMap.restrictHom {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (S : Set V) (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) : (G.restrict S hS).Hom G

The inclusion of a restriction of G into G is a homomorphism.

@[simp]

theorem Cslib.RotationMap.restrictHom_apply {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (S : Set V) (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) (v : ↑S) : (G.restrictHom S hS) v = ↑v

The inclusion of a restriction maps a vertex to itself.

@[simp]

theorem Cslib.RotationMap.coe_neighbor_restrict {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (S : Set V) (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) (v : ↑S) (i : D) : ↑((G.restrict S hS).neighbor v i) = G.neighbor (↑v) i

The neighbors in a restriction are the neighbors in G.

theorem Cslib.RotationMap.reachable_neighbor {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (v : V) (i : D) : G.toSimpleGraph.Reachable v (G.neighbor v i)

Every neighbor of a vertex is reachable from it in the simple graph of G.

theorem Cslib.RotationMap.Hom.reachable_map {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') {u v : V} (h : G.toSimpleGraph.Reachable u v) : G'.toSimpleGraph.Reachable (φ u) (φ v)

A homomorphism maps reachable vertices to reachable vertices.

theorem Cslib.RotationMap.Hom.exists_reachable_apply_eq {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') {u : V} {w : W} (h : G'.toSimpleGraph.Reachable (φ u) w) : ∃ (v : V), G.toSimpleGraph.Reachable u v ∧ φ v = w

Lifting walks along a homomorphism: every vertex reachable from the image of u is the image of a vertex reachable from u.

theorem Cslib.RotationMap.Hom.reachable_apply_iff {V : Type u_1} {W : Type u_2} {D : Type u_4} {G : RotationMap V D} {G' : RotationMap W D} (φ : G.Hom G') (hφ : Function.Injective ⇑φ) {u v : V} : G'.toSimpleGraph.Reachable (φ u) (φ v) ↔ G.toSimpleGraph.Reachable u v

Along an injective homomorphism, the images of two vertices are reachable from each other exactly when the vertices are.

theorem Cslib.RotationMap.reachable_neighbor_pow_of_forall {V : Type u_1} {W : Type u_2} {D : Type u_4} {D' : Type u_6} (G : RotationMap V D) (G' : RotationMap W D') (π : W → V) (hπ : ∀ (x : W) (i : D'), G.toSimpleGraph.Reachable (π x) (π (G'.neighbor x i))) (t : ℕ) (x : W) (k : Fin t → D') : G.toSimpleGraph.Reachable (π x) (π ((G'.pow t).neighbor x k))

If every edge of G' joins vertices whose images under π are reachable from each other in G, so does every walk.

theorem Cslib.RotationMap.mem_of_reachable {V : Type u_1} {D : Type u_4} (G : RotationMap V D) {S : Set V} (hS : ∀ v ∈ S, ∀ (i : D), G.neighbor v i ∈ S) {u v : V} (hu : u ∈ S) (h : G.toSimpleGraph.Reachable u v) : v ∈ S

A set of vertices closed under taking neighbors contains every vertex reachable from it.

theorem Cslib.RotationMap.neighbor_mem_setOf_reachable {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (s v : V) : v ∈ {v : V | G.toSimpleGraph.Reachable s v} → ∀ (i : D), G.neighbor v i ∈ {v : V | G.toSimpleGraph.Reachable s v}

The vertices reachable from s are closed under taking neighbors.

def Cslib.RotationMap.componentGraph {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (s : V) : RotationMap (↑{v : V | G.toSimpleGraph.Reachable s v}) D

The connected component of s in G, as a rotation map: the restriction of G to the vertices reachable from s.

def Cslib.RotationMap.componentHom {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (s : V) : (G.componentGraph s).Hom G

The inclusion of the connected component of s into G.

@[simp]

theorem Cslib.RotationMap.componentHom_apply {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (s : V) (v : ↑{v : V | G.toSimpleGraph.Reachable s v}) : (G.componentHom s) v = ↑v

The inclusion of the connected component of s maps a vertex to itself.

theorem Cslib.RotationMap.preconnected_componentGraph {V : Type u_1} {D : Type u_4} (G : RotationMap V D) (s : V) : (G.componentGraph s).toSimpleGraph.Preconnected

The connected component of a vertex is connected.