Catalog/Sparsity/ShallowMinor/Full.lean

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3
4	namespace Catalog.Sparsity.ShallowMinor
5
6	/-- A depth-`d` minor model of `H` in `G`.
7
8	For each vertex of `H` we choose a branch set in `G` together with a fixed
9	center. Every vertex of the branch set is connected to the center by a path of
10	length at most `d` that stays inside the branch set; distinct branch sets are
11	disjoint; and every edge of `H` is witnessed by an edge of `G` between the
12	corresponding branch sets. (Defs 1.10, 2.2-2.4) -/
13	structure ShallowMinorModel {V W : Type} (H : SimpleGraph W) (G : SimpleGraph V)
14	(d : ℕ) where
15	branchSet : W → Set V
16	center : W → V
17	center_mem : ∀ v, center v ∈ branchSet v
18	branchDisjoint : ∀ u v, u ≠ v → Disjoint (branchSet u) (branchSet v)
19	branchRadius : ∀ v x, x ∈ branchSet v →
20	∃ p : G.Walk (center v) x, p.IsPath ∧ p.length ≤ d ∧
21	∀ w ∈ p.support, w ∈ branchSet v
22	branchEdge : ∀ u v, H.Adj u v →
23	∃ x ∈ branchSet u, ∃ y ∈ branchSet v, G.Adj x y
24
25	/-- `H` is a depth-`d` minor of `G`. -/
26	def IsShallowMinor {V W : Type} (H : SimpleGraph W) (G : SimpleGraph V)
27	(d : ℕ) : Prop :=
28	Nonempty (ShallowMinorModel H G d)
29
30	end Catalog.Sparsity.ShallowMinor
31