acyclic graphs and finite paths

Stream: new members

[Christopher Schmidt]

Hello everyone,
Is there something regarding: "an acyclic graph only has finitely many paths from a to b (a and b fixed vertices)" in mathlib? I could not find something useful.

[Kyle Miller]

It's got that there is at most one path docs#simple_graph.is_acyclic_iff_path_unique

[Christopher Schmidt]

Kyle Miller schrieb:

It's got that there is at most one path docs#simple_graph.is_acyclic_iff_path_unique

Oh..how could I miss that. I guess because I thought of directed graphs where its not unique and therefore did not have a look at this.
Thank you.

[Kyle Miller]

@Christopher Schmidt Just so you know, for simple graphs this is a more complicated theorem to prove because walks are able to travel across edges in either direction. For acyclic directed graphs, I'd take a completely different approach:

1. Show that every a walk p in an acyclic directed graph has p.length < card V. Do it by contradiction: otherwise there is a duplicate vertex in the support, and you can form a cycle.
2. Reproduce relevant material from this section to get finsets/fintypes for all the walks of a given length in a directed graph with a finite vertex set. (Or a locally finite directed graph if you want to do a light generalization -- it's not harder to do this.)
3. Use 1 to show that the set of all walks between two vertices is finite, since you can take a finite union of finite sets from 2.

[Christopher Schmidt]

Kyle Miller schrieb:

Christopher Schmidt Just so you know, for simple graphs this is a more complicated theorem to prove because walks are able to travel across edges in either direction. For acyclic directed graphs, I'd take a completely different approach:

1. Show that every a walk p in an acyclic directed graph has p.length < card V. Do it by contradiction: otherwise there is a duplicate vertex in the support, and you can form a cycle.
2. Reproduce relevant material from this section to get finsets/fintypes for all the walks of a given length in a directed graph with a finite vertex set. (Or a locally finite directed graph if you want to do a light generalization -- it's not harder to do this.)
3. Use 1 to show that the set of all walks between two vertices is finite, since you can take a finite union of finite sets from 2.

Amazing, thanks for the idea of the approach! I will give it a shot.