Definition
A graph H is a depth-r minor of a graph G if H can be obtained from G by deleting vertices and edges and contracting pairwise disjoint connected subgraphs of radius at most r. A graph class is nowhere dense if for every depth r there is a t such that no member has the complete graph on t vertices as a depth-r minor.
Lean source view on GitHub
| 1 | import Lax5.GraphClasses |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Walk.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Nowhere dense graph classes |
| 7 | type: definition |
| 8 | --- |
| 9 | A graph *H* is a depth-*r* minor of a graph *G* if *H* can be obtained |
| 10 | from *G* by deleting vertices and edges and contracting pairwise |
| 11 | disjoint connected subgraphs of radius at most *r*. A graph class is |
| 12 | nowhere dense if for every depth *r* there is a *t* such that no member |
| 13 | has the complete graph on *t* vertices as a depth-*r* minor. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | A depth-`r` minor is witnessed by a `ShallowMinorModel`: pairwise |
| 18 | disjoint branch sets, one per vertex of `H`, and an edge of `G` between |
| 19 | the branch sets of any two adjacent vertices of `H`. The radius |
| 20 | condition — every element of a branch set is reached from its center by |
| 21 | a walk of length at most `r` staying inside the branch set — subsumes |
| 22 | connectivity of the branch sets, so no separate connectivity field is |
| 23 | carried. `center_mem` is not derivable: it also rules out empty branch |
| 24 | sets, as the standard definition requires. `⊤ : SimpleGraph (Fin t)` is |
| 25 | mathlib's complete graph. |
| 26 | -/ |
| 27 | |
| 28 | namespace Lax5.NowhereDenseClasses |
| 29 | |
| 30 | open Lax5.GraphClasses |
| 31 | |
| 32 | /-- A model of `H` as a depth-`r` minor of `G`: pairwise disjoint branch |
| 33 | sets, each spanned by walks of length at most `r` from a center vertex |
| 34 | (hence connected of radius at most `r`), with an edge of `G` between the |
| 35 | branch sets of any two adjacent vertices of `H`. -/ |
| 36 | structure ShallowMinorModel {V W : Type*} (r : ℕ) (H : SimpleGraph W) |
| 37 | (G : SimpleGraph V) where |
| 38 | /-- The branch set of each vertex of `H`. -/ |
| 39 | branch : W → Set V |
| 40 | /-- The center of each branch set. -/ |
| 41 | center : W → V |
| 42 | /-- Centers lie in their branch sets (so branch sets are nonempty). -/ |
| 43 | center_mem : ∀ u, center u ∈ branch u |
| 44 | /-- Distinct branch sets are disjoint. -/ |
| 45 | disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v) |
| 46 | /-- Every vertex of a branch set is reached from the center by a walk |
| 47 | of length at most `r` inside the branch set. -/ |
| 48 | radius_le : ∀ u, ∀ x ∈ branch u, ∃ w : G.Walk (center u) x, |
| 49 | w.length ≤ r ∧ ∀ y ∈ w.support, y ∈ branch u |
| 50 | /-- Adjacent vertices of `H` have adjacent branch sets. -/ |
| 51 | adj : ∀ u v, H.Adj u v → ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y |
| 52 | |
| 53 | /-- `H` is a minor of `G` at depth `r`. -/ |
| 54 | def HasShallowMinor {V W : Type*} (G : SimpleGraph V) (r : ℕ) |
| 55 | (H : SimpleGraph W) : Prop := |
| 56 | Nonempty (ShallowMinorModel r H G) |
| 57 | |
| 58 | /-- A graph class is nowhere dense if for every depth `r` some complete |
| 59 | graph is not a depth-`r` minor of any member. -/ |
| 60 | def NowhereDense (C : GraphClass) : Prop := |
| 61 | ∀ r : ℕ, ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → |
| 62 | ¬ HasShallowMinor G r (⊤ : SimpleGraph (Fin t)) |
| 63 | |
| 64 | end Lax5.NowhereDenseClasses |
| 65 |
Formalization notes
A depth-r minor is witnessed by a ShallowMinorModel: pairwise
disjoint branch sets, one per vertex of H, and an edge of G between
the branch sets of any two adjacent vertices of H. The radius
condition — every element of a branch set is reached from its center by
a walk of length at most r staying inside the branch set — subsumes
connectivity of the branch sets, so no separate connectivity field is
carried. center_mem is not derivable: it also rules out empty branch
sets, as the standard definition requires. ⊤ : SimpleGraph (Fin t) is
mathlib's complete graph.