Catalog/Sparsity/ShallowTopologicalMinor/Contract.lean

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3	import Mathlib.Data.Sym.Sym2
4	import Catalog.Sparsity.ShallowMinor.Contract
5
6	namespace Catalog.Sparsity.ShallowTopologicalMinor
7
8	open Catalog.Sparsity.ShallowMinor
9
10	/-- A depth-`d` topological minor model of `H` in `G`.
11
12	Each vertex of `H` is mapped injectively to a branch vertex of `G`. Every edge
13	of `H` is routed by a path between the corresponding branch vertices, of length
14	at most `2d + 1`. Internal routed vertices avoid all branch vertices, and the
15	internal vertices of routed paths for distinct edges are disjoint.
16	(Defs 1.12, 2.15-2.16) -/
17	structure ShallowTopologicalMinorModel {V W : Type}
18	(H : SimpleGraph W) (G : SimpleGraph V) (d : ℕ) where
19	branchVertex : W ↪ V
20	edgeTail : H.edgeSet → W
21	edgeTail_mem : ∀ e : H.edgeSet, edgeTail e ∈ (e : Sym2 W)
22	edgePath : ∀ e : H.edgeSet,
23	G.Walk (branchVertex (edgeTail e))
24	(branchVertex (Sym2.Mem.other (edgeTail_mem e)))
25	edgePath_isPath : ∀ e, (edgePath e).IsPath
26	edgePath_length : ∀ e, (edgePath e).length ≤ 2 * d + 1
27	edgePath_interior_avoids_branch :
28	∀ e {x : V},
29	x ∈ (edgePath e).support →
30	x ≠ branchVertex (edgeTail e) →
31	x ≠ branchVertex (Sym2.Mem.other (edgeTail_mem e)) →
32	∀ w : W, x ≠ branchVertex w
33	edgePath_interior_disjoint :
34	∀ e e' {x : V},
35	e ≠ e' →
36	x ∈ (edgePath e).support →
37	x ∈ (edgePath e').support →
38	x ≠ branchVertex (edgeTail e) →
39	x ≠ branchVertex (Sym2.Mem.other (edgeTail_mem e)) →
40	x ≠ branchVertex (edgeTail e') →
41	x ≠ branchVertex (Sym2.Mem.other (edgeTail_mem e')) →
42	False
43
44	/-- `H` is a depth-`d` topological minor of `G`. -/
45	def IsShallowTopologicalMinor {V W : Type}
46	(H : SimpleGraph W) (G : SimpleGraph V) (d : ℕ) : Prop :=
47	Nonempty (ShallowTopologicalMinorModel H G d)
48
49	/-- Every depth-`d` shallow topological minor is a depth-`d` shallow minor. -/
50	axiom shallowTopologicalMinor_toShallowMinor
51	{V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ} :
52	IsShallowTopologicalMinor H G d → IsShallowMinor H G d
53
54	end Catalog.Sparsity.ShallowTopologicalMinor
55