Lax12.NowhereDenseClasses

Nowhere dense graph classes

concepts/Lax12/NowhereDenseClasses.lean · lax-12

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 2 of the paper of lax-242665, An Introduction to Lax

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.

The source lecture notes give these as Definitions 2.3 and 2.6 of Chapter 1 (2019/20 edition), writing H ⪯r G for the depth-r minor relation. Nowhere denseness is stated there as ωr(C) < ∞ for every r, with the excluded-clique form used here spelled out immediately after as an equivalent.

Lean source view on GitHub

1	import Lax12.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	The source lecture notes give these as Definitions 2.3 and 2.6 of
16	Chapter 1 (2019/20 edition), writing H ⪯_r G for the depth-r
17	minor relation. Nowhere denseness is stated there as ω_r(C) < ∞ for
18	every r, with the excluded-clique form used here spelled out
19	immediately after as an equivalent.
20
21	# Formalization notes
22
23	A depth-`r` minor is witnessed by a `ShallowMinorModel`: pairwise
24	disjoint branch sets, one per vertex of `H`, and an edge of `G` between
25	the branch sets of any two adjacent vertices of `H`. The radius
26	condition — every element of a branch set is reached from its center by
27	a walk of length at most `r` staying inside the branch set — subsumes
28	connectivity of the branch sets, so no separate connectivity field is
29	carried. `center_mem` is not derivable: it also rules out empty branch
30	sets, as the standard definition requires. `⊤ : SimpleGraph (Fin t)` is
31	mathlib's complete graph.
32	-/
33
34	namespace Lax12.NowhereDenseClasses
35
36	open Lax12.GraphClasses
37
38	/-- A model of `H` as a depth-`r` minor of `G`: pairwise disjoint branch
39	sets, each spanned by walks of length at most `r` from a center vertex
40	(hence connected of radius at most `r`), with an edge of `G` between the
41	branch sets of any two adjacent vertices of `H`. -/
42	structure ShallowMinorModel {V W : Type*} (r : ℕ) (H : SimpleGraph W)
43	(G : SimpleGraph V) where
44	/-- The branch set of each vertex of `H`. -/
45	branch : W → Set V
46	/-- The center of each branch set. -/
47	center : W → V
48	/-- Centers lie in their branch sets (so branch sets are nonempty). -/
49	center_mem : ∀ u, center u ∈ branch u
50	/-- Distinct branch sets are disjoint. -/
51	disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v)
52	/-- Every vertex of a branch set is reached from the center by a walk
53	of length at most `r` inside the branch set. -/
54	radius_le : ∀ u, ∀ x ∈ branch u, ∃ w : G.Walk (center u) x,
55	w.length ≤ r ∧ ∀ y ∈ w.support, y ∈ branch u
56	/-- Adjacent vertices of `H` have adjacent branch sets. -/
57	adj : ∀ u v, H.Adj u v → ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y
58
59	/-- `H` is a minor of `G` at depth `r`. -/
60	def HasShallowMinor {V W : Type*} (G : SimpleGraph V) (r : ℕ)
61	(H : SimpleGraph W) : Prop :=
62	Nonempty (ShallowMinorModel r H G)
63
64	/-- A graph class is nowhere dense if for every depth `r` some complete
65	graph is not a depth-`r` minor of any member. -/
66	def NowhereDense (C : GraphClass) : Prop :=
67	∀ r : ℕ, ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
68	¬ HasShallowMinor G r (⊤ : SimpleGraph (Fin t))
69
70	end Lax12.NowhereDenseClasses
71

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.

Builds on

Lax12.GraphClasses

Used by

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

Loading discussion…

Lax Lean Archive