Concatenation along prescribed endpoints #
Induced graphs covering every vertex and edge can share vertices. If every shared vertex lies in both bags at the join, concatenate their decompositions without increasing the common bag-size bound.
theorem
Algebraic.Cutwidth.PathDecomposition.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
Concatenate induced decompositions whose adjoining bags contain every shared vertex. The last bag is inherited from the right decomposition.
theorem
Algebraic.Cutwidth.PathDecomposition.exists_glue_embeddings
{U V W : Type}
{G : SimpleGraph U}
{J : SimpleGraph V}
{H : SimpleGraph W}
(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
Concatenate two induced copies covering all vertices and edges. Shared vertices must belong to the adjoining bags, expressed through their embeddings.
theorem
Algebraic.Cutwidth.PathDecomposition.exists_attach
{V W : Type}
{G : SimpleGraph V}
{H : SimpleGraph W}
(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)
:
Attach an induced subgraph along a boundary X. The remaining graph
ends at the part of X outside the copy, and all edges leaving the copy meet
X. Padding the copy's bags by X gives the final endpoint X.