definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A graph is a minor of a graph when every vertex of can be represented by a nonempty connected branch set of vertices of , distinct branch sets are disjoint, and every edge of is represented by an edge of between the corresponding branch sets.
This is the standard branch-set definition. It applies to arbitrary simple graphs; the polynomial grid-minor theorem later specializes the host graph to a finite vertex type.
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Graph minors |
| 6 | type: definition |
| 7 | --- |
| 8 | A graph \(H\) is a minor of a graph \(G\) when every vertex of \(H\) can be |
| 9 | represented by a nonempty connected branch set of vertices of \(G\), distinct |
| 10 | branch sets are disjoint, and every edge of \(H\) is represented by an edge of |
| 11 | \(G\) between the corresponding branch sets. |
| 12 | |
| 13 | This is the standard branch-set definition. It applies to arbitrary simple |
| 14 | graphs; the polynomial grid-minor theorem later specializes the host graph to |
| 15 | a finite vertex type. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax17.Minor |
| 19 | |
| 20 | universe u v |
| 21 | |
| 22 | /-- Branch-set data witnessing that `H` is a minor of `G`. -/ |
| 23 | structure Model {W : Type u} {V : Type v} |
| 24 | (H : SimpleGraph W) (G : SimpleGraph V) where |
| 25 | /-- The branch set representing each vertex of `H`. -/ |
| 26 | branchSet : W → Set V |
| 27 | /-- Every branch set is nonempty. -/ |
| 28 | branch_nonempty : ∀ w : W, (branchSet w).Nonempty |
| 29 | /-- Every branch set induces a connected graph in `G`. -/ |
| 30 | branch_connected : |
| 31 | ∀ w : W, (G.induce (branchSet w)).Connected |
| 32 | /-- Branch sets representing distinct vertices are disjoint. -/ |
| 33 | branch_disjoint : |
| 34 | ∀ ⦃x y : W⦄, x ≠ y → Disjoint (branchSet x) (branchSet y) |
| 35 | /-- Every edge of `H` is represented by an edge between branch sets. -/ |
| 36 | adjacent : |
| 37 | ∀ ⦃x y : W⦄, H.Adj x y → |
| 38 | ∃ a ∈ branchSet x, ∃ b ∈ branchSet y, G.Adj a b |
| 39 | |
| 40 | /-- `H` is a graph minor of `G`. -/ |
| 41 | def IsMinor {W : Type u} {V : Type v} |
| 42 | (H : SimpleGraph W) (G : SimpleGraph V) : Prop := |
| 43 | Nonempty (Model H G) |
| 44 | |
| 45 | end Lax17.Minor |
| 46 |
Builds on
none
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments