Concatenating overlapping induced decompositions #
Two induced graphs cover the vertices and edges. Their path decompositions can be concatenated if every shared vertex belongs to the adjoining bags. The last bag of the right decomposition is retained, and no bag grows.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_glue
{W : Type}
{H : SimpleGraph W}
{A B : Set W}
(D : PathDecomposition (SimpleGraph.induce A H))
(E : PathDecomposition (SimpleGraph.induce B H))
(cover : ∀ (w : W), w ∈ A ∨ w ∈ B)
(edges : ∀ (u v : W), H.Adj u v → u ∈ A ∧ v ∈ A ∨ u ∈ B ∧ v ∈ B)
{X : Finset ↑A}
(hend : D.EndsAt X)
{Y Z : Finset ↑B}
(hstart : E.StartsAt Y)
(hend' : E.EndsAt Z)
(overlap : ∀ (w : W) (ha : w ∈ A) (hb : w ∈ B), ⟨w, ha⟩ ∈ X ∧ ⟨w, hb⟩ ∈ Y)
{b : ℕ}
(leftBound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
(rightBound : ∀ (i : Fin E.length), (E.bag i).card ≤ b)
:
∃ (F : PathDecomposition H),
F.EndsAt (Finset.map (Function.Embedding.subtype fun (x : W) => x ∈ B) Z) ∧ ∀ (i : Fin F.length), (F.bag i).card ≤ b
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_glue_embeddings
{W : Type}
{H : SimpleGraph W}
{U V : Type}
{G : SimpleGraph U}
{J : SimpleGraph V}
(D : PathDecomposition G)
(E : PathDecomposition J)
(f : G ↪g H)
(g : J ↪g H)
(cover : ∀ (w : W), w ∈ Set.range ⇑f ∨ w ∈ Set.range ⇑g)
(edges : ∀ (u v : W), H.Adj u v → u ∈ Set.range ⇑f ∧ v ∈ Set.range ⇑f ∨ u ∈ Set.range ⇑g ∧ v ∈ Set.range ⇑g)
{X : Finset U}
(hend : D.EndsAt X)
{Y Z : Finset V}
(hstart : E.StartsAt Y)
(hend' : E.EndsAt Z)
(overlap : ∀ (u : U) (v : V), f u = g v → u ∈ X ∧ v ∈ Y)
{b : ℕ}
(leftBound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
(rightBound : ∀ (i : Fin E.length), (E.bag i).card ≤ b)
:
∃ (F : PathDecomposition H), F.EndsAt (Finset.map g.toEmbedding Z) ∧ ∀ (i : Fin F.length), (F.bag i).card ≤ b
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_attach
{W : Type}
{H : SimpleGraph W}
{V : Type}
{G : SimpleGraph V}
(f : G ↪g H)
(X : Finset W)
(D : PathDecomposition (SimpleGraph.induce {w : W | w ∉ Set.range ⇑f} H))
(E : PathDecomposition G)
(hend : D.EndsAt (Finset.subtype (fun (x : W) => x ∉ Set.range ⇑f) X))
(neighbors : ∀ (u : V) (v : W), H.Adj (f u) v → v ∈ Set.range ⇑f ∨ v ∈ X)
{b c : ℕ}
(leftBound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
(rightBound : ∀ (i : Fin E.length), (E.bag i).card ≤ c)
: