Graph connectivity #
In a simple graph,
-
A walk is a finite sequence of adjacent vertices, and can be thought of equally well as a sequence of directed edges.
-
A trail is a walk whose edges each appear no more than once.
-
A path is a trail whose vertices appear no more than once.
-
A cycle is a nonempty trail whose first and last vertices are the same and whose vertices except for the first appear no more than once.
Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."
Some definitions and theorems have inspiration from multigraph counterparts in [Cho94].
Main definitions #
-
simple_graph.walk
(with accompanying pattern definitionssimple_graph.walk.nil'
andsimple_graph.walk.cons'
) -
simple_graph.walk.is_trail
,simple_graph.walk.is_path
, andsimple_graph.walk.is_cycle
. -
simple_graph.walk.map
andsimple_graph.path.map
for the induced map on walks, given an (injective) graph homomorphism. -
simple_graph.reachable
for the relation of whether there exists a walk between a given pair of vertices -
simple_graph.preconnected
andsimple_graph.connected
are predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty. -
simple_graph.subgraph.connected
gives subgraphs the connectivity predicate viasimple_graph.subgraph.coe
. -
simple_graph.connected_component
is the type of connected components of a given graph.
Tags #
walks, trails, paths, circuits, cycles
- nil : Π {V : Type u} {G : simple_graph V} {u : V}, G.walk u u
- cons : Π {V : Type u} {G : simple_graph V} {u v w : V}, G.adj u v → G.walk v w → G.walk u w
A walk is a sequence of adjacent vertices. For vertices u v : V
,
the type walk u v
consists of all walks starting at u
and ending at v
.
We say that a walk visits the vertices it contains. The set of vertices a
walk visits is simple_graph.walk.support
.
See simple_graph.walk.nil'
and simple_graph.walk.cons'
for patterns that
can be useful in definitions since they make the vertices explicit.
Instances for simple_graph.walk
- simple_graph.walk.has_sizeof_inst
- simple_graph.walk.inhabited
Equations
Pattern to get walk.nil
with the vertex as an explicit argument.
Pattern to get walk.cons
with the vertices as explicit arguments.
The length of a walk is the number of edges/darts along it.
Equations
- (simple_graph.walk.cons _x_2 q).length = q.length.succ
- simple_graph.walk.nil.length = 0
The concatenation of two compatible walks.
Equations
- (simple_graph.walk.cons h p).append q = simple_graph.walk.cons h (p.append q)
- simple_graph.walk.nil.append q = q
The concatenation of the reverse of the first walk with the second walk.
Equations
- (simple_graph.walk.cons h p).reverse_aux q = p.reverse_aux (simple_graph.walk.cons _ q)
- simple_graph.walk.nil.reverse_aux q = q
The walk in reverse.
Equations
Get the n
th vertex from a walk, where n
is generally expected to be
between 0
and p.length
, inclusive.
If n
is greater than or equal to p.length
, the result is the path's endpoint.
Equations
- (simple_graph.walk.cons _x q).get_vert (n + 1) = q.get_vert n
- (simple_graph.walk.cons _x _x_1).get_vert 0 = u
- simple_graph.walk.nil.get_vert _x = u
The support
of a walk is the list of vertices it visits in order.
Equations
- (simple_graph.walk.cons h p).support = u :: p.support
- simple_graph.walk.nil.support = [u]
The darts
of a walk is the list of darts it visits in order.
The edges
of a walk is the list of edges it visits in order.
This is defined to be the list of edges underlying simple_graph.walk.darts
.
Equations
Every edge in a walk's edge list is an edge of the graph.
It is written in this form (rather than using ⊆
) to avoid unsightly coercions.
Trails, paths, circuits, cycles #
A trail is a walk with no repeating edges.
A path is a walk with no repeating vertices.
Use simple_graph.walk.is_path.mk'
for a simpler constructor.
- to_trail : p.is_trail
- ne_nil : p ≠ simple_graph.walk.nil
A circuit at u : V
is a nonempty trail beginning and ending at u
.
- to_circuit : p.is_circuit
- support_nodup : p.support.tail.nodup
A cycle at u : V
is a circuit at u
whose only repeating vertex
is u
(which appears exactly twice).
Walk decompositions #
Given a vertex in the support of a path, give the path up until (and including) that vertex.
Equations
- (simple_graph.walk.cons r p).take_until u h = dite (v = u) (λ (hx : v = u), eq.rec (λ (h : v ∈ (simple_graph.walk.cons r p).support), simple_graph.walk.nil) hx h) (λ (hx : ¬v = u), simple_graph.walk.cons r (p.take_until u _))
- simple_graph.walk.nil.take_until u h = _.mpr simple_graph.walk.nil
Given a vertex in the support of a path, give the path from (and including) that vertex to the end. In other words, drop vertices from the front of a path until (and not including) that vertex.
Equations
- (simple_graph.walk.cons r p).drop_until u h = dite (v = u) (λ (hx : v = u), eq.rec (λ (h : v ∈ (simple_graph.walk.cons r p).support), simple_graph.walk.cons r p) hx h) (λ (hx : ¬v = u), p.drop_until u _)
- simple_graph.walk.nil.drop_until u h = _.mpr simple_graph.walk.nil
The take_until
and drop_until
functions split a walk into two pieces.
The lemma count_support_take_until_eq_one
specifies where this split occurs.
Rotate a loop walk such that it is centered at the given vertex.
Equations
- c.rotate h = (c.drop_until u h).append (c.take_until u h)
Type of paths #
The type for paths between two vertices.
The length-0 path at a vertex.
Equations
The length-1 path between a pair of adjacent vertices.
Equations
The reverse of a path is another path. See also simple_graph.walk.reverse
.
Walks to paths #
Given a walk, produces a walk from it by bypassing subwalks between repeated vertices.
The result is a path, as shown in simple_graph.walk.bypass_is_path
.
This is packaged up in simple_graph.walk.to_path
.
Equations
- (simple_graph.walk.cons ha p).bypass = let p' : G.walk a_39 v := p.bypass in dite (u ∈ p'.support) (λ (hs : u ∈ p'.support), p'.drop_until u hs) (λ (hs : u ∉ p'.support), simple_graph.walk.cons ha p')
- simple_graph.walk.nil.bypass = simple_graph.walk.nil
Given a walk, produces a path with the same endpoints using simple_graph.walk.bypass
.
Mapping paths #
Given a graph homomorphism, map walks to walks.
Given an injective graph homomorphism, map paths to paths.
Equations
- simple_graph.path.map f hinj p = ⟨simple_graph.walk.map f ↑p, _⟩
Given a graph embedding, map paths to paths.
Equations
Deleting edges #
Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.
Equations
Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted.
This is an abbreviation for simple_graph.walk.to_delete_edges
.
reachable
and connected
#
Two vertices are reachable if there is a walk between them.
This is equivalent to relation.refl_trans_gen
of G.adj
.
See simple_graph.reachable_iff_refl_trans_gen
.
The equivalence relation on vertices given by simple_graph.reachable
.
A graph is preconnected if every pair of vertices is reachable from one another.
Equations
- G.preconnected = ∀ (u v : V), G.reachable u v
- preconnected : G.preconnected
- nonempty : nonempty V
A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.
There is a has_coe_to_fun
instance so that h u v
can be used instead
of h.preconnected u v
.
Instances for simple_graph.connected
Equations
The quotient of V
by the simple_graph.reachable
relation gives the connected
components of a graph.
Equations
- G.connected_component = quot G.reachable
Instances for simple_graph.connected_component
Gives the connected component containing a particular vertex.
Equations
- G.connected_component_mk v = quot.mk G.reachable v
The connected_component
specialization of quot.lift
. Provides the stronger
assumption that the vertices are connected by a path.
Equations
- simple_graph.connected_component.lift f h = quot.lift f _
A subgraph is connected if it is connected as a simple graph.
Walks of a given length #
The finset
of length-n
walks from u
to v
.
This is used to give {p : G.walk u v | p.length = n}
a fintype
instance, and it
can also be useful as a recursive description of this set when V
is finite.
See simple_graph.coe_finset_walk_length_eq
for the relationship between this finset
and
the set of length-n
walks.
Equations
- G.finset_walk_length (n + 1) u v = finset.univ.bUnion (λ (w : V), dite (G.adj u w) (λ (h : G.adj u w), finset.map {to_fun := λ (p : G.walk w v), simple_graph.walk.cons h p, inj' := _} (G.finset_walk_length n w v)) (λ (h : ¬G.adj u w), ∅))
- G.finset_walk_length 0 u v = dite (u = v) (λ (h : u = v), eq.rec {simple_graph.walk.nil} _) (λ (h : ¬u = v), ∅)
Equations
- G.fintype_set_walk_length u v n = fintype.subtype (G.finset_walk_length n u v) _