Acyclic graphs and trees

This module introduces acyclic graphs (a.k.a. forests) and trees.

Main definitions

• SimpleGraph.IsAcyclic is a predicate for a graph having no cyclic walks.
• SimpleGraph.IsTree is a predicate for a graph being a tree (a connected acyclic graph).

Main statements

• SimpleGraph.isAcyclic_iff_path_unique characterizes acyclicity in terms of uniqueness of paths between pairs of vertices.
• SimpleGraph.isAcyclic_iff_forall_edge_isBridge characterizes acyclicity in terms of every edge being a bridge edge.
• SimpleGraph.isTree_iff_existsUnique_path characterizes trees in terms of existence and uniqueness of paths between pairs of vertices from a nonempty vertex type.

References

The structure of the proofs for SimpleGraph.IsAcyclic and SimpleGraph.IsTree, including supporting lemmas about SimpleGraph.IsBridge, generally follows the high-level description for these theorems for multigraphs from [Chou1994].

Tags

acyclic graphs, trees

def SimpleGraph.IsAcyclic {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is acyclic (or a forest) if it has no cycles.

structure SimpleGraph.IsTree {V : Type u_1} (G : SimpleGraph V) : Prop

A tree is a connected acyclic graph.

• isConnected : G.Connected

  Graph is connected.

• IsAcyclic : G.IsAcyclic

  Graph is acyclic.

theorem SimpleGraph.isTree_iff {V : Type u_1} (G : SimpleGraph V) : G.IsTree ↔ G.Connected ∧ G.IsAcyclic

@[simp]

theorem SimpleGraph.isAcyclic_bot {V : Type u_1} : ⊥.IsAcyclic

theorem SimpleGraph.IsAcyclic.comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) (h : G'.IsAcyclic) : G.IsAcyclic

A graph that has an injective homomorphism to an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.embedding {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (h : G'.IsAcyclic) : G.IsAcyclic

theorem SimpleGraph.Iso.isAcyclic_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') : G.IsAcyclic ↔ G'.IsAcyclic

Isomorphic graphs are acyclic together.

theorem SimpleGraph.Iso.isTree_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') : G.IsTree ↔ G'.IsTree

Isomorphic graphs are trees together.

theorem SimpleGraph.IsAcyclic.of_map {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V ↪ V') (h : (SimpleGraph.map f G).IsAcyclic) : G.IsAcyclic

theorem SimpleGraph.IsAcyclic.of_comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V' ↪ V) (h : G.IsAcyclic) : (SimpleGraph.comap (⇑f) G).IsAcyclic

theorem SimpleGraph.IsAcyclic.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (s : Set V) : (SimpleGraph.induce s G).IsAcyclic

A graph induced from an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.subgraph {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (H : G.Subgraph) : H.coe.IsAcyclic

A subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.anti {V : Type u_1} {G G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) : G.IsAcyclic

A spanning subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.isAcyclic_sSup_of_isAcyclic_directedOn {V : Type u_1} (Hs : Set (SimpleGraph V)) (h_acyc : ∀ H ∈ Hs, H.IsAcyclic) (h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) => x1 ≤ x2) Hs) : (sSup Hs).IsAcyclic

The directed supremum of acyclic graphs is acylic.

theorem SimpleGraph.exists_maximal_isAcyclic_of_le_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (hHG : H ≤ G) (hH : H.IsAcyclic) : ∃ (H' : SimpleGraph V), H ≤ H' ∧ Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) H'

Every acyclic subgraph H ≤ G is contained in a maximal such subgraph.

theorem SimpleGraph.IsAcyclic.isTree_connectedComponent {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (c : G.ConnectedComponent) : c.toSimpleGraph.IsTree

A connected component of an acyclic graph is a tree.

theorem SimpleGraph.IsAcyclic.of_subsingleton {V : Type u_1} [Subsingleton V] {G : SimpleGraph V} : G.IsAcyclic

theorem SimpleGraph.Subgraph.isAcyclic_coe_bot {V : Type u_1} (G : SimpleGraph V) : ⊥.coe.IsAcyclic

theorem SimpleGraph.IsTree.of_subsingleton {V : Type u_1} [Nonempty V] [Subsingleton V] {G : SimpleGraph V} : G.IsTree

theorem SimpleGraph.IsTree.coe_singletonSubgraph {V : Type u_1} (G : SimpleGraph V) (v : V) : (G.singletonSubgraph v).coe.IsTree

theorem SimpleGraph.IsTree.coe_subgraphOfAdj {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : (G.subgraphOfAdj h).coe.IsTree

theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge {V : Type u_1} {G : SimpleGraph V} : G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge {V : Type u_1} {G : SimpleGraph V} : G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

theorem SimpleGraph.IsAcyclic.path_unique {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p q : G.Path v w) : p = q

theorem SimpleGraph.isAcyclic_of_path_unique {V : Type u_1} {G : SimpleGraph V} (h : ∀ (v w : V) (p q : G.Path v w), p = q) : G.IsAcyclic

theorem SimpleGraph.isAcyclic_iff_path_unique {V : Type u_1} {G : SimpleGraph V} : G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

theorem SimpleGraph.IsAcyclic.mem_support_of_ne_mem_support_of_adj_of_isPath {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∉ q.support) : w ∈ p.support

theorem SimpleGraph.IsAcyclic.ne_mem_support_of_support_of_adj_of_isPath {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hw : w ∈ p.support) : v ∉ q.support

theorem SimpleGraph.IsAcyclic.path_concat {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∈ q.support) : q = p.concat hadj

theorem SimpleGraph.isTree_iff_existsUnique_path {V : Type u_1} {G : SimpleGraph V} : G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

theorem SimpleGraph.IsTree.existsUnique_path {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (v w : V) : ∃! p : G.Walk v w, p.IsPath

theorem SimpleGraph.IsAcyclic.isPath_iff_isChain {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) : p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) => x1 ≠ x2) p.edges

theorem SimpleGraph.IsAcyclic.isPath_iff_isTrail {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) : p.IsPath ↔ p.IsTrail

theorem SimpleGraph.IsTree.card_edgeFinset {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Fintype ↑G.edgeSet] (hG : G.IsTree) : G.edgeFinset.card + 1 = Fintype.card V

theorem SimpleGraph.isTree_of_minimal_connected {V : Type u_1} {G : SimpleGraph V} (h : Minimal Connected G) : G.IsTree

A minimally connected graph is a tree.

theorem SimpleGraph.isTree_iff_minimal_connected {V : Type u_1} {G : SimpleGraph V} : G.IsTree ↔ Minimal Connected G

theorem SimpleGraph.isAcyclic_add_edge_iff_of_not_reachable {V : Type u_1} {G : SimpleGraph V} (x y : V) (hxy : ¬G.Reachable x y) : (G ⊔ fromEdgeSet {s(x, y)}).IsAcyclic ↔ G.IsAcyclic

Adding an edge to an acyclic graph preserves acyclicity if the endpoints are not reachable.

theorem SimpleGraph.reachable_eq_of_maximal_isAcyclic {V : Type u_1} {G : SimpleGraph V} (F : SimpleGraph V) (h : Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) F) : F.Reachable = G.Reachable

The reachability relation of a maximal acyclic subgraph agrees with that of the larger graph.

theorem SimpleGraph.maximal_isAcyclic_iff_reachable_eq {V : Type u_1} {G F : SimpleGraph V} (hF : F ≤ G) (hF' : F.IsAcyclic) : Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) F ↔ F.Reachable = G.Reachable

A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph.

theorem SimpleGraph.Connected.maximal_le_isAcyclic_iff_isTree {V : Type u_1} {G T : SimpleGraph V} (hG : G.Connected) (hT : T ≤ G) : Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

A subgraph of a connected graph is maximal acyclic iff it is a tree.

@[simp]

theorem SimpleGraph.maximal_isAcyclic_iff_isTree {V : Type u_1} [Nonempty V] {T : SimpleGraph V} : Maximal IsAcyclic T ↔ T.IsTree

theorem SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (hH_le : H ≤ G) (hH_isAcyclic : H.IsAcyclic) : ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable

Every acyclic subgraph can be extended to a spanning forest.

theorem SimpleGraph.exists_isAcyclic_reachable_eq_le {V : Type u_1} {G : SimpleGraph V} : ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable

Every graph has a spanning forest.

theorem SimpleGraph.Connected.exists_isTree_le_of_le_of_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (h : G.Connected) (hH_le : H ≤ G) (hH_isAcyclic : H.IsAcyclic) : ∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree

Every acyclic subgraph of a connected graph can be extended to a spanning tree.

theorem SimpleGraph.Connected.exists_isTree_le {V : Type u_1} {G : SimpleGraph V} (h : G.Connected) : ∃ T ≤ G, T.IsTree

Every connected graph has a spanning tree.

theorem SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one {V : Type u_1} {G : SimpleGraph V} (h : G.Connected) : Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Every connected graph on n vertices has at least n-1 edges.

theorem SimpleGraph.isTree_iff_connected_and_card {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V

theorem SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} (h : G.IsTree) [Fintype V] [Nontrivial V] [DecidableRel G.Adj] : G.minDegree = 1

The minimum degree of all vertices in a nontrivial tree is one.

theorem SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Nontrivial V] [DecidableRel G.Adj] (h : G.IsTree) : ∃ (v : V), G.degree v = 1

A nontrivial tree has a vertex of degree one.

theorem SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) {v : V} [Fintype ↑(G.neighborSet v)] (hdeg : G.degree v = 1) : (induce {v}ᶜ G).Connected

The graph resulting from removing a vertex of degree one from a connected graph is connected.

theorem SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (hconn : G.Connected) : ∃ (v : V), (induce {v}ᶜ G).Connected

A finite nontrivial connected graph contains a vertex that leaves the graph connected if removed.

theorem SimpleGraph.Connected.exists_preconnected_induce_compl_singleton_of_finite {V : Type u_1} {G : SimpleGraph V} [Finite V] (hconn : G.Connected) : ∃ (v : V), (induce {v}ᶜ G).Preconnected

A finite connected graph contains a vertex that leaves the graph preconnected if removed.

theorem SimpleGraph.IsAcyclic.dist_ne_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} (hadj : G.Adj v w) (hreach : G.Reachable u v) : G.dist u v ≠ G.dist u w

theorem SimpleGraph.IsTree.dist_ne_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) : G.dist u v ≠ G.dist u w

theorem SimpleGraph.IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) (u : V) {v w : V} (hadj : G.Adj v w) (hreach : G.Reachable u v) : G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

theorem SimpleGraph.IsTree.dist_eq_dist_add_one_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) : G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

noncomputable def SimpleGraph.IsTree.coloringTwoOfVert {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) : G.Coloring (Fin 2)

The unique two-coloring of a tree that colors the given vertex with zero

noncomputable def SimpleGraph.IsTree.coloringTwo {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) : G.Coloring (Fin 2)

Arbitrary coloring with two colors for a tree

theorem SimpleGraph.IsTree.isBipartite {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) : G.IsBipartite

noncomputable def SimpleGraph.IsAcyclic.coloringTwoOfVerts {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) (verts : G.ConnectedComponent → V) (h : ∀ (C : G.ConnectedComponent), verts C ∈ C) : G.Coloring (Fin 2)

The unique two-coloring of a forest that colors the given vertices with zero

noncomputable def SimpleGraph.IsAcyclic.coloringTwo {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) : G.Coloring (Fin 2)

Arbitrary coloring with two colors for a forest

theorem SimpleGraph.IsAcyclic.isBipartite {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) : G.IsBipartite