Endpoint operations for path decompositions #
Appending a subset of the last bag preserves the interval property. A vertex deleted from the graph can be restored in a new last bag when that bag already contains all its neighbors. These are the deletion steps in Fomin and Høie's endpoint decomposition argument.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_endsAt_subset
{W : Type}
{H : SimpleGraph W}
(D : PathDecomposition H)
{X Y : Finset W}
(hend : D.EndsAt Y)
(hXY : X ⊆ Y)
{b : ℕ}
(bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
:
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_restoreVertex
{W : Type}
{H : SimpleGraph W}
(v : W)
(D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H))
{Y : Finset { w : W // w ≠ v }}
(hend : D.EndsAt Y)
(neighbors : ∀ (w : W), H.Adj v w → w ∈ Finset.map (Function.Embedding.subtype fun (x : W) => x ≠ v) Y)
{b : ℕ}
(bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
(hY : Y.card + 1 ≤ b)
:
∃ (D' : PathDecomposition H),
D'.EndsAt (insert v (Finset.map (Function.Embedding.subtype fun (x : W) => x ≠ v) Y)) ∧ ∀ (i : Fin D'.length), (D'.bag i).card ≤ b
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_endsAt_of_delete
{W : Type}
{H : SimpleGraph W}
(v : W)
{X Y : Finset W}
(hv : v ∈ Y)
(D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H))
(hend : D.EndsAt (Finset.subtype (fun (x : W) => x ≠ v) Y))
(neighbors : ∀ (w : W), H.Adj v w → w ∈ Y)
(hXY : X ⊆ Y)
{b : ℕ}
(bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
(hY : Y.card ≤ b)
:
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_addVertex
{W : Type}
{H : SimpleGraph W}
(v : W)
(D : PathDecomposition (SimpleGraph.induce {w : W | w ≠ v} H))
{b : ℕ}
(bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
: