Trail, Path, and Cycle #
In a simple graph,
A trail is a walk whose edges each appear no more than once.
A circuit is a nonempty trail whose first and last vertices are the same.
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 #
SimpleGraph.Walk.IsTrail
,SimpleGraph.Walk.IsPath
, andSimpleGraph.Walk.IsCycle
.SimpleGraph.Path.map
for the induced map on paths, given an (injective) graph homomorphism.
Tags #
trails, paths, circuits, cycles
Trails, paths, circuits, cycles #
A trail is a walk with no repeating edges.
Instances For
A path is a walk with no repeating vertices.
Use SimpleGraph.Walk.IsPath.mk'
for a simpler constructor.
- edges_nodup : p.edges.Nodup
Instances For
A circuit at u : V
is a nonempty trail beginning and ending at u
.
- edges_nodup : p.edges.Nodup
Instances For
A cycle at u : V
is a circuit at u
whose only repeating vertex
is u
(which appears exactly twice).
- edges_nodup : p.edges.Nodup
Instances For
About paths #
Equations
About cycles #
Alias of SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one
.
Walk decompositions #
Taking a strict initial segment of a path removes the end vertex from the support.
Alias of SimpleGraph.Walk.endpoint_notMem_support_takeUntil
.
Taking a strict initial segment of a path removes the end vertex from the support.
Type of paths #
The length-0 path at a vertex.
Equations
Instances For
The length-1 path between a pair of adjacent vertices.
Equations
Instances For
The reverse of a path is another path. See also SimpleGraph.Walk.reverse
.
Instances For
Alias of SimpleGraph.Path.notMem_edges_of_loop
.
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 SimpleGraph.Walk.bypass_isPath
.
This is packaged up in SimpleGraph.Walk.toPath
.
Equations
- SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
- (SimpleGraph.Walk.cons ha p).bypass = if hs : u ∈ p.bypass.support then p.bypass.dropUntil u hs else SimpleGraph.Walk.cons ha p.bypass
Instances For
Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass
.
Instances For
Mapping paths #
Alias of the reverse direction of SimpleGraph.Walk.map_isTrail_iff_of_injective
.
Alias of the reverse direction of SimpleGraph.Walk.map_isCycle_iff_of_injective
.
Alias of the forward direction of SimpleGraph.Walk.mapLe_isTrail
.
Alias of the reverse direction of SimpleGraph.Walk.mapLe_isTrail
.
Alias of the forward direction of SimpleGraph.Walk.mapLe_isPath
.
Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath
.
Alias of the reverse direction of SimpleGraph.Walk.mapLe_isCycle
.
Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle
.
Given an injective graph homomorphism, map paths to paths.
Equations
- SimpleGraph.Path.map f hinj p = ⟨SimpleGraph.Walk.map f ↑p, ⋯⟩
Instances For
Given a graph embedding, map paths to paths.