Removing designated edges from cycles #
Choose a largest set of designated edges whose deletion preserves reachability. Every remaining designated edge is then a bridge. The number removed is bounded by the original cycle rank, since the surviving graph still has the same connected components.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.exists_delete_to_bridges
{V : Type}
[Fintype V]
(B : SimpleGraph V)
(eligible : Finset (Sym2 V))
(edges : eligible ⊆ B.edgeFinset)
:
∃ removed ⊆ eligible,
(B.deleteEdges ↑removed).Reachable = B.Reachable ∧ (∀ e ∈ eligible \ removed, (B.deleteEdges ↑removed).IsBridge e) ∧ removed.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.cycle_contains_boundary_of_meets_region
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{P : Finset V}
(connected : (SimpleGraph.induce {v : V | v ∈ P} B).Connected)
(degree : ∀ v ∈ P, B.degree v ≤ 2)
{u : V}
{p : B.Walk u u}
(cycle : p.IsCycle)
(meets : ∃ v ∈ P, v ∈ p.support)
{e : Sym2 V}
(boundary : e ∈ B.cutFinset P)
:
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.exists_delete_avoiding_regions
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{ι : Type}
[Fintype ι]
(P : ι → Finset V)
(connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected)
(degree : ∀ (i : ι), ∀ v ∈ P i, B.degree v ≤ 2)
(chosen : ι → Sym2 V)
(boundary : ∀ (i : ι), chosen i ∈ B.cutFinset (P i))
:
∃ removed ⊆ Finset.image chosen Finset.univ,
(B.deleteEdges ↑removed).Reachable = B.Reachable ∧ removed.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent ∧ ∀ (u : V) (p : (B.deleteEdges ↑removed).Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.exists_isolate_regions_without_cycles
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{ι : Type}
[Fintype ι]
(P : ι → Finset V)
(connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected)
(degree : ∀ (i : ι), ∀ v ∈ P i, B.degree v ≤ 2)
(chosen : ι → Sym2 V)
(injective : Function.Injective chosen)
(boundary : ∀ (i : ι), chosen i ∈ B.cutFinset (P i))
:
∃ (indices : Finset ι),
indices.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent ∧ (B.deleteEdges ↑(Finset.image chosen indices)).Reachable = B.Reachable ∧ ∀ (u : V) (p : (B.deleteEdges ↑(indices.biUnion fun (i : ι) => B.cutFinset (P i))).Walk u u),
p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support