Cycles, Spanning Trees and Spanning Forests of a Multigraph
Lax630294.SpanningStructures · concepts/Lax630294/SpanningStructures.lean · lax-630294
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Let be a multigraph and let be a set of edges of ; we identify with the spanning subgraph of that keeps all vertices of and only the edges in . The components of are the connected components of this subgraph; every vertex of lies in a component, even if it is incident to no edge of .
A set of edges is simple if it contains no loop and no two parallel edges. A simple set is acyclic if the subgraph it forms has no cycle, and it is a tree if it is acyclic and connected. A spanning tree of is a simple set of edges of forming a tree on all vertices of . A spanning forest with components of is a simple acyclic set of edges of with exactly components.
A cycle of length consists of pairwise distinct vertices and pairwise distinct edges such that joins and , with indices taken modulo . Its edge set is .
Concept map
In the paper
- page 3 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.Graph.Delete |
| 2 | import Mathlib.Combinatorics.Graph.Simple |
| 3 | import Mathlib.Combinatorics.SimpleGraph.Acyclic |
| 4 | import Mathlib.Data.Set.Card |
| 5 | import Mathlib.Data.ENat.Basic |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Cycles, Spanning Trees and Spanning Forests of a Multigraph |
| 10 | type: definition |
| 11 | --- |
| 12 | |
| 13 | Let `G` be a multigraph and let `F` be a set of edges of `G`; we identify `F` |
| 14 | with the spanning subgraph of `G` that keeps all vertices of `G` and only the |
| 15 | edges in `F`. The *components* of `F` are the connected components of this |
| 16 | subgraph; every vertex of `G` lies in a component, even if it is incident to no |
| 17 | edge of `F`. |
| 18 | |
| 19 | A set `F` of edges is *simple* if it contains no loop and no two parallel edges. |
| 20 | A simple set `F` is *acyclic* if the subgraph it forms has no cycle, and it is a |
| 21 | *tree* if it is acyclic and connected. A *spanning tree* of `G` is a simple set of |
| 22 | edges of `G` forming a tree on all vertices of `G`. A *spanning forest with `k` |
| 23 | components* of `G` is a simple acyclic set of edges of `G` with exactly `k` |
| 24 | components. |
| 25 | |
| 26 | A *cycle of length `n ≥ 1`* consists of `n` pairwise distinct vertices |
| 27 | `v₀, …, vₙ₋₁` and `n` pairwise distinct edges `e₀, …, eₙ₋₁` such that `eᵢ` joins |
| 28 | `vᵢ` and `vᵢ₊₁`, with indices taken modulo `n`. Its edge set is `{e₀, …, eₙ₋₁}`. |
| 29 | |
| 30 | # Formalization notes |
| 31 | |
| 32 | The multigraph is Mathlib's `Graph α β`. Connectivity, components, trees and |
| 33 | acyclicity are taken from Mathlib's theory of simple graphs, applied to |
| 34 | `Graph.toSimpleGraph` of the spanning subgraph `G.restrict F`; this forgets loops |
| 35 | and parallel edges. Requiring `(G.restrict F).Simple` restores them, so that a loop |
| 36 | or a pair of parallel edges in `F` is never accepted as part of a tree or a forest |
| 37 | (these are the cycles of length one and two). Cycles are given by an explicit cyclic |
| 38 | sequence indexed by `ZMod n`; a cycle of length one is a loop and a cycle of length |
| 39 | two is a pair of parallel edges. The number of components is an extended natural number (`ENat.card`), so |
| 40 | that infinitely many components are not mistaken for a finite number. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax630294.SpanningStructures |
| 44 | |
| 45 | open Graph |
| 46 | |
| 47 | variable {α β : Type*} |
| 48 | |
| 49 | /-- The simple graph underlying the spanning subgraph of `G` with edge set `F`. -/ |
| 50 | abbrev underlying (G : Graph α β) (F : Set β) : SimpleGraph V(G) := |
| 51 | (G.restrict F).toSimpleGraph |
| 52 | |
| 53 | /-- The vertices of `G` incident to an edge of `F`. -/ |
| 54 | def incidentVertices (G : Graph α β) (F : Set β) : Set α := |
| 55 | {x | ∃ e ∈ F, G.Inc e x} |
| 56 | |
| 57 | /-- `C` is the edge set of a cycle of `G` of some length `n ≥ 1`: there are |
| 58 | pairwise distinct vertices `v 0, …, v (n - 1)` and pairwise distinct edges |
| 59 | `e 0, …, e (n - 1)` such that `e i` links `v i` and `v (i + 1)`, with indices |
| 60 | taken modulo `n`, and `C` consists of these edges. Its length is `C.encard`. -/ |
| 61 | def IsCycle (G : Graph α β) (C : Set β) : Prop := |
| 62 | ∃ n : ℕ, 0 < n ∧ ∃ (v : ZMod n → α) (e : ZMod n → β), |
| 63 | Function.Injective v ∧ Function.Injective e ∧ |
| 64 | (∀ i, G.IsLink (e i) (v i) (v (i + 1))) ∧ Set.range e = C |
| 65 | |
| 66 | /-- `T` is a spanning tree of `G`. -/ |
| 67 | def IsSpanningTree (G : Graph α β) (T : Set β) : Prop := |
| 68 | T ⊆ E(G) ∧ (G.restrict T).Simple ∧ (underlying G T).IsTree |
| 69 | |
| 70 | /-- `F` is a spanning forest of `G` with exactly `k` components. -/ |
| 71 | def IsSpanningForest (G : Graph α β) (F : Set β) (k : ℕ) : Prop := |
| 72 | F ⊆ E(G) ∧ (G.restrict F).Simple ∧ (underlying G F).IsAcyclic ∧ |
| 73 | ENat.card (underlying G F).ConnectedComponent = k |
| 74 | |
| 75 | end Lax630294.SpanningStructures |
| 76 |
Formalization notes
The multigraph is Mathlib's . Connectivity, components, trees and acyclicity are taken from Mathlib's theory of simple graphs, applied to of the spanning subgraph ; this forgets loops and parallel edges. Requiring restores them, so that a loop or a pair of parallel edges in is never accepted as part of a tree or a forest (these are the cycles of length one and two). Cycles are given by an explicit cyclic sequence indexed by ; a cycle of length one is a loop and a cycle of length two is a pair of parallel edges. The number of components is an extended natural number (), so that infinitely many components are not mistaken for a finite number.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments