Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/ShallowTopologicalMinor/Full.lean
1import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2import Mathlib.Combinatorics.SimpleGraph.Paths
3import Mathlib.Data.Sym.Sym2
4import Catalog.Sparsity.ShallowMinor.Full
5
6namespace Catalog.Sparsity.ShallowTopologicalMinor
7
8open Catalog.Sparsity.ShallowMinor
9
10/-- A depth-`d` topological minor model of `H` in `G`.
11
12Each vertex of `H` is mapped injectively to a branch vertex of `G`. Every edge
13of `H` is routed by a path between the corresponding branch vertices, of length
14at most `2d + 1`. Internal routed vertices avoid all branch vertices, and the
15internal vertices of routed paths for distinct edges are disjoint.
16(Defs 1.12, 2.15-2.16) -/
17structure 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`. -/
45def IsShallowTopologicalMinor {V W : Type}
46 (H : SimpleGraph W) (G : SimpleGraph V) (d : ℕ) : Prop :=
47 Nonempty (ShallowTopologicalMinorModel H G d)
48
49noncomputable def ShallowTopologicalMinorModel.ofSubgraph
50 {V W : Type} {H : SimpleGraph W} {G G' : SimpleGraph V} {d : ℕ}
51 (m : ShallowTopologicalMinorModel H G d)
52 (hsub : ∀ {u v}, G.Adj u v → G'.Adj u v) :
53 ShallowTopologicalMinorModel H G' d :=
54 { branchVertex := m.branchVertex
55 edgeTail := m.edgeTail
56 edgeTail_mem := m.edgeTail_mem
57 edgePath := fun e => by
58 let p := m.edgePath e
59 have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by
60 intro e' he'
61 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he'
62 revert hmem
63 refine e'.ind ?_
64 intro a b hab
65 exact show G'.Adj a b by exact hsub hab
66 exact p.transfer G' hedge
67 edgePath_isPath := by
68 intro e
69 let p := m.edgePath e
70 have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by
71 intro e' he'
72 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he'
73 revert hmem
74 refine e'.ind ?_
75 intro a b hab
76 exact show G'.Adj a b by exact hsub hab
77 simpa [p] using (m.edgePath_isPath e).transfer hedge
78 edgePath_length := by
79 intro e
80 let p := m.edgePath e
81 have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by
82 intro e' he'
83 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he'
84 revert hmem
85 refine e'.ind ?_
86 intro a b hab
87 exact show G'.Adj a b by exact hsub hab
88 rw [show ((p.transfer G' hedge)).length = p.length by
89 rw [SimpleGraph.Walk.length_transfer]]
90 exact m.edgePath_length e
91 edgePath_interior_avoids_branch := by
92 intro e x hx htail hhead w
93 let p := m.edgePath e
94 have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by
95 intro e' he'
96 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he'
97 revert hmem
98 refine e'.ind ?_
99 intro a b hab
100 exact show G'.Adj a b by exact hsub hab
101 rw [show (p.transfer G' hedge).support = p.support by
102 rw [SimpleGraph.Walk.support_transfer]] at hx
103 exact m.edgePath_interior_avoids_branch e hx htail hhead w
104 edgePath_interior_disjoint := by
105 intro e e' x hne hx hx' htail hhead htail' hhead'
106 let p := m.edgePath e
107 let p' := m.edgePath e'
108 have hedge : ∀ e'' ∈ p.edges, e'' ∈ G'.edgeSet := by
109 intro e'' he''
110 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he''
111 revert hmem
112 refine e''.ind ?_
113 intro a b hab
114 exact show G'.Adj a b by exact hsub hab
115 have hedge' : ∀ e'' ∈ p'.edges, e'' ∈ G'.edgeSet := by
116 intro e'' he''
117 have hmem := SimpleGraph.Walk.edges_subset_edgeSet p' he''
118 revert hmem
119 refine e''.ind ?_
120 intro a b hab
121 exact show G'.Adj a b by exact hsub hab
122 rw [show (p.transfer G' hedge).support = p.support by
123 rw [SimpleGraph.Walk.support_transfer]] at hx
124 rw [show (p'.transfer G' hedge').support = p'.support by
125 rw [SimpleGraph.Walk.support_transfer]] at hx'
126 exact m.edgePath_interior_disjoint e e' hne hx hx' htail hhead htail' hhead' }
127
128theorem shallowTopologicalMinor_of_subgraph
129 {V W : Type} {H : SimpleGraph W} {G G' : SimpleGraph V} {d : ℕ}
130 (hsub : ∀ {u v}, G.Adj u v → G'.Adj u v) :
131 IsShallowTopologicalMinor H G d → IsShallowTopologicalMinor H G' d := by
132 rintro ⟨m⟩
133 exact ⟨m.ofSubgraph hsub⟩
134
135private def routedPathSplit {V : Type} {G : SimpleGraph V} {u v : V}
136 (p : G.Walk u v) (d : ℕ) : ℕ :=
137 min d (p.length - 1)
138
139private def routedPrefixVertices {V : Type} {G : SimpleGraph V} {u v : V}
140 (p : G.Walk u v) (d : ℕ) : Set V :=
141 {x | ∃ i ≤ routedPathSplit p d, x = p.getVert i}
142
143private def routedSuffixVertices {V : Type} {G : SimpleGraph V} {u v : V}
144 (p : G.Walk u v) (d : ℕ) : Set V :=
145 {x | ∃ i, routedPathSplit p d + 1 ≤ i ∧ i ≤ p.length ∧ x = p.getVert i}
146
147private def topologicalBranchSet {V W : Type}
148 {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
149 (m : ShallowTopologicalMinorModel H G d) (w : W) : Set V :=
150 {x | x = m.branchVertex w ∨
151 ∃ e : H.edgeSet,
152 (m.edgeTail e = w ∧ x ∈ routedPrefixVertices (m.edgePath e) d) ∨
153 (Sym2.Mem.other (m.edgeTail_mem e) = w ∧ x ∈ routedSuffixVertices (m.edgePath e) d)}
154
155private theorem mem_topologicalBranchSet_center
156 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
157 (m : ShallowTopologicalMinorModel H G d) (w : W) :
158 m.branchVertex w ∈ topologicalBranchSet m w := by
159 left
160 rfl
161
162private theorem edgePath_internal_not_branchVertex
163 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
164 (m : ShallowTopologicalMinorModel H G d) (e : H.edgeSet) {i : ℕ}
165 (hi0 : 0 < i) (hil : i < (m.edgePath e).length) :
166 ∀ w : W, (m.edgePath e).getVert i ≠ m.branchVertex w := by
167 intro w
168 have hp := m.edgePath_isPath e
169 have hne_tail : (m.edgePath e).getVert i ≠ m.branchVertex (m.edgeTail e) := by
170 intro hEq
171 have hi_eq : i = 0 := (hp.getVert_eq_start_iff hil.le).mp (by simpa using hEq)
172 omega
173 have hne_head : (m.edgePath e).getVert i ≠
174 m.branchVertex (Sym2.Mem.other (m.edgeTail_mem e)) := by
175 intro hEq
176 have hi_eq : i = (m.edgePath e).length :=
177 (hp.getVert_eq_end_iff hil.le).mp (by simpa using hEq)
178 omega
179 exact m.edgePath_interior_avoids_branch e ((m.edgePath e).getVert_mem_support i)
180 hne_tail hne_head w
181
182private theorem mem_topologicalBranchSet_noncenter
183 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
184 (m : ShallowTopologicalMinorModel H G d) {w : W} {x : V}
185 (hx : x ∈ topologicalBranchSet m w) (hxc : x ≠ m.branchVertex w) :
186 ∃ e : H.edgeSet, ∃ i : ℕ,
187 x = (m.edgePath e).getVert i ∧
188 0 < i ∧ i < (m.edgePath e).length ∧
189 ((m.edgeTail e = w ∧ i ≤ routedPathSplit (m.edgePath e) d) ∨
190 (Sym2.Mem.other (m.edgeTail_mem e) = w ∧
191 routedPathSplit (m.edgePath e) d + 1 ≤ i)) := by
192 rcases hx with rfl | ⟨e, hx⟩
193 · exact (hxc rfl).elim
194 · rcases hx with ⟨hw, hx⟩ | ⟨hw, hx⟩
195 · rcases hx with ⟨i, hi, rfl⟩
196 have hi_pos : 0 < i := by
197 by_contra hi0
198 apply hxc
199 have : i = 0 := Nat.eq_zero_of_not_pos hi0
200 simpa [hw, this] using (m.edgePath e).getVert_zero
201 refine ⟨e, i, rfl, hi_pos, ?_, Or.inl ⟨hw, hi⟩⟩
202 · have hi' : i ≤ (m.edgePath e).length - 1 := le_trans hi (Nat.min_le_right _ _)
203 have hlen : 1 < (m.edgePath e).length := by
204 exact Nat.sub_pos_iff_lt.mp (lt_of_lt_of_le hi_pos hi')
205 have hsucc : i + 1 ≤ (m.edgePath e).length :=
206 (Nat.le_sub_iff_add_le hlen.le).mp hi'
207 exact lt_of_lt_of_le (Nat.lt_succ_self i) hsucc
208 · rcases hx with ⟨i, hi, hilen, rfl⟩
209 refine ⟨e, i, rfl, ?_, ?_, Or.inr ⟨hw, hi⟩⟩
210 · omega
211 · by_contra hlt
212 have hi_eq : i = (m.edgePath e).length :=
213 le_antisymm hilen (Nat.not_lt.mp hlt)
214 apply hxc
215 simpa [hw, hi_eq] using (m.edgePath e).getVert_length
216
217private theorem topologicalBranchSet_disjoint
218 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
219 (m : ShallowTopologicalMinorModel H G d) :
220 ∀ u v, u ≠ v → Disjoint (topologicalBranchSet m u) (topologicalBranchSet m v) := by
221 intro u v huv
222 refine Set.disjoint_left.mpr ?_
223 intro x hxu hxv
224 by_cases hxu0 : x = m.branchVertex u
225 · by_cases hxv0 : x = m.branchVertex v
226 · exact huv (m.branchVertex.injective (hxu0.symm.trans hxv0))
227 · obtain ⟨e, i, hxi, hi0, hil, _⟩ := mem_topologicalBranchSet_noncenter m hxv hxv0
228 exact (edgePath_internal_not_branchVertex m e hi0 hil u) (hxi.symm.trans hxu0)
229 · by_cases hxv0 : x = m.branchVertex v
230 · obtain ⟨e, i, hxi, hi0, hil, _⟩ := mem_topologicalBranchSet_noncenter m hxu hxu0
231 exact (edgePath_internal_not_branchVertex m e hi0 hil v) (hxi.symm.trans hxv0)
232 · obtain ⟨e, i, hxi, hi0, hil, hside_u⟩ := mem_topologicalBranchSet_noncenter m hxu hxu0
233 obtain ⟨e', j, hxj, hj0, hjl, hside_v⟩ := mem_topologicalBranchSet_noncenter m hxv hxv0
234 by_cases he : e = e'
235 · subst e'
236 have hp := m.edgePath_isPath e
237 have hij : i = j := hp.getVert_injOn (by simp [hil.le]) (by simp [hjl.le])
238 (hxi.symm.trans hxj)
239 rcases hside_u with ⟨hu, hi_le⟩ | ⟨hu, hi_ge⟩
240 · rcases hside_v with ⟨hv, hj_le⟩ | ⟨hv, hj_ge⟩
241 · exact huv (hu.symm.trans hv)
242 · have : i < j := by omega
243 exact this.ne hij
244 · rcases hside_v with ⟨hv, hj_le⟩ | ⟨hv, hj_ge⟩
245 · have : j < i := by omega
246 exact this.ne hij.symm
247 · exact huv (hu.symm.trans hv)
248 · have hx_support : x ∈ (m.edgePath e).support := by
249 rw [hxi]
250 exact (m.edgePath e).getVert_mem_support i
251 have hx_support' : x ∈ (m.edgePath e').support := by
252 rw [hxj]
253 exact (m.edgePath e').getVert_mem_support j
254 have hne_tail : x ≠ m.branchVertex (m.edgeTail e) := by
255 simpa [hxi] using (edgePath_internal_not_branchVertex m e hi0 hil (m.edgeTail e))
256 have hne_head : x ≠ m.branchVertex (Sym2.Mem.other (m.edgeTail_mem e)) := by
257 simpa [hxi] using
258 (edgePath_internal_not_branchVertex m e hi0 hil
259 (Sym2.Mem.other (m.edgeTail_mem e)))
260 have hne_tail' : x ≠ m.branchVertex (m.edgeTail e') := by
261 simpa [hxj] using
262 (edgePath_internal_not_branchVertex m e' hj0 hjl (m.edgeTail e'))
263 have hne_head' : x ≠ m.branchVertex (Sym2.Mem.other (m.edgeTail_mem e')) := by
264 simpa [hxj] using
265 (edgePath_internal_not_branchVertex m e' hj0 hjl
266 (Sym2.Mem.other (m.edgeTail_mem e')))
267 exact m.edgePath_interior_disjoint e e' he hx_support hx_support'
268 hne_tail hne_head hne_tail' hne_head'
269
270private theorem topologicalBranchSet_radius
271 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
272 (m : ShallowTopologicalMinorModel H G d) :
273 ∀ v x, x ∈ topologicalBranchSet m v →
274 ∃ p : G.Walk (m.branchVertex v) x, p.IsPath ∧ p.length ≤ d ∧
275 ∀ w ∈ p.support, w ∈ topologicalBranchSet m v := by
276 intro v x hx
277 rcases hx with rfl | ⟨e, hx⟩
278 · refine ⟨SimpleGraph.Walk.nil, by simp, by simp, ?_⟩
279 intro w hw
280 simp at hw
281 simpa [hw] using mem_topologicalBranchSet_center m v
282 · rcases hx with ⟨hv, hx⟩ | ⟨hv, hx⟩
283 · rcases hx with ⟨i, hi, rfl⟩
284 let p := m.edgePath e
285 have hi_len : i ≤ p.length := by
286 exact le_trans hi (le_trans (Nat.min_le_right d (p.length - 1)) (Nat.sub_le _ _))
287 refine ⟨(p.take i).copy (by simpa [hv]) rfl, ?_, ?_, ?_⟩
288 · simpa [p] using (m.edgePath_isPath e).take i
289 · rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.take_length, Nat.min_eq_left hi_len]
290 exact le_trans hi (Nat.min_le_left d (p.length - 1))
291 · intro w hw
292 have hw' : w ∈ (p.take i).support := by simpa using hw
293 rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hw' with ⟨j, rfl, hj⟩
294 have hj' : j ≤ i := by
295 rwa [SimpleGraph.Walk.take_length, Nat.min_eq_left hi_len] at hj
296 right
297 refine ⟨e, Or.inl ?_⟩
298 refine ⟨hv, ⟨j, le_trans hj' hi, ?_⟩⟩
299 rw [SimpleGraph.Walk.take_getVert]
300 simpa [p, Nat.min_eq_right hj']
301 · rcases hx with ⟨i, hi_split, hi_len, rfl⟩
302 let p := m.edgePath e
303 have hi_split' : routedPathSplit p d + 1 ≤ i := by simpa [p] using hi_split
304 have hi_len' : i ≤ p.length := by simpa [p] using hi_len
305 have hp_len : p.length ≤ 2 * d + 1 := by simpa [p] using m.edgePath_length e
306 have hdrop_len : p.length - i ≤ d := by
307 dsimp [routedPathSplit] at hi_split'
308 by_cases hmin : d ≤ p.length - 1
309 · rw [Nat.min_eq_left hmin] at hi_split'
310 omega
311 · rw [Nat.min_eq_right (Nat.le_of_not_ge hmin)] at hi_split'
312 omega
313 refine ⟨((p.drop i).reverse).copy (by simpa [hv]) rfl, ?_, ?_, ?_⟩
314 · simpa [p] using ((m.edgePath_isPath e).drop i).reverse
315 · rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.length_reverse, SimpleGraph.Walk.drop_length]
316 exact hdrop_len
317 · intro w hw
318 have hw' : w ∈ ((p.drop i).reverse).support := by simpa using hw
319 rw [SimpleGraph.Walk.support_reverse] at hw'
320 have hw'' : w ∈ (p.drop i).support := List.mem_reverse.mp hw'
321 rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hw'' with ⟨j, rfl, hj⟩
322 have hij : i + j ≤ p.length := by
323 rw [SimpleGraph.Walk.drop_length] at hj
324 simpa [Nat.add_comm] using Nat.add_le_of_le_sub hi_len' hj
325 right
326 refine ⟨e, Or.inr ?_⟩
327 refine ⟨hv, ⟨i + j, le_trans hi_split' (Nat.le_add_right _ _), hij, ?_⟩⟩
328 rw [SimpleGraph.Walk.drop_getVert]
329
330private theorem topologicalBranchSet_edge
331 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
332 (m : ShallowTopologicalMinorModel H G d) :
333 ∀ u v, H.Adj u v →
334 ∃ x ∈ topologicalBranchSet m u, ∃ y ∈ topologicalBranchSet m v, G.Adj x y := by
335 intro u v huv
336 let e : H.edgeSet := ⟨s(u, v), huv⟩
337 let p := m.edgePath e
338 let s := routedPathSplit p d
339 have htail_mem : m.edgeTail e ∈ (e : Sym2 W) := m.edgeTail_mem e
340 have hother_ne : Sym2.Mem.other htail_mem ≠ m.edgeTail e :=
341 H.edge_other_ne e.property htail_mem
342 have hp_not_nil : ¬ p.Nil := by
343 apply SimpleGraph.Walk.not_nil_of_ne
344 intro hEq
345 exact hother_ne (m.branchVertex.injective hEq.symm)
346 have hs_lt : s < p.length := by
347 have hp_pos : 0 < p.length := SimpleGraph.Walk.not_nil_iff_lt_length.mp hp_not_nil
348 dsimp [s, routedPathSplit]
349 exact lt_of_le_of_lt (Nat.min_le_right _ _) (Nat.sub_lt hp_pos (by decide))
350 have htail_cases : m.edgeTail e = u ∨ m.edgeTail e = v := by
351 simpa [e] using htail_mem
352 rcases htail_cases with htail_u | htail_v
353 · have hother_v : Sym2.Mem.other htail_mem = v := by
354 have hmem : Sym2.Mem.other htail_mem ∈ (e : Sym2 W) := Sym2.other_mem htail_mem
355 have hne : Sym2.Mem.other htail_mem ≠ u := by simpa [htail_u] using hother_ne
356 have hmem' : Sym2.Mem.other htail_mem = u ∨ Sym2.Mem.other htail_mem = v := by
357 simpa [e] using hmem
358 exact hmem'.resolve_left hne
359 refine ⟨p.getVert s, ?_, p.getVert (s + 1), ?_, p.adj_getVert_succ hs_lt⟩
360 · right
361 refine ⟨e, Or.inl ?_⟩
362 refine ⟨htail_u, ?_⟩
363 exact ⟨s, le_rfl, rfl⟩
364 · right
365 refine ⟨e, Or.inr ?_⟩
366 refine ⟨hother_v, ?_⟩
367 exact ⟨s + 1, le_rfl, Nat.succ_le_of_lt hs_lt, rfl⟩
368 · have hother_u : Sym2.Mem.other htail_mem = u := by
369 have hmem : Sym2.Mem.other htail_mem ∈ (e : Sym2 W) := Sym2.other_mem htail_mem
370 have hne : Sym2.Mem.other htail_mem ≠ v := by simpa [htail_v] using hother_ne
371 have hmem' : Sym2.Mem.other htail_mem = u ∨ Sym2.Mem.other htail_mem = v := by
372 simpa [e] using hmem
373 exact hmem'.resolve_right hne
374 refine ⟨p.getVert (s + 1), ?_, p.getVert s, ?_, (p.adj_getVert_succ hs_lt).symm⟩
375 · right
376 refine ⟨e, Or.inr ?_⟩
377 refine ⟨hother_u, ?_⟩
378 exact ⟨s + 1, le_rfl, Nat.succ_le_of_lt hs_lt, rfl⟩
379 · right
380 refine ⟨e, Or.inl ?_⟩
381 refine ⟨htail_v, ?_⟩
382 exact ⟨s, le_rfl, rfl⟩
383
384private def ShallowTopologicalMinorModel.toShallowMinorModel
385 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
386 (m : ShallowTopologicalMinorModel H G d) : ShallowMinorModel H G d :=
387 { branchSet := topologicalBranchSet m
388 center := m.branchVertex
389 center_mem := mem_topologicalBranchSet_center m
390 branchDisjoint := topologicalBranchSet_disjoint m
391 branchRadius := topologicalBranchSet_radius m
392 branchEdge := topologicalBranchSet_edge m }
393
394/-- Every depth-`d` shallow topological minor is a depth-`d` shallow minor. -/
395theorem shallowTopologicalMinor_toShallowMinor
396 {V W : Type} {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ} :
397 IsShallowTopologicalMinor H G d → IsShallowMinor H G d := by
398 rintro ⟨m⟩
399 exact ⟨m.toShallowMinorModel⟩
400
401end Catalog.Sparsity.ShallowTopologicalMinor
402