Identifying region vertices in the boundary quotient #
Disjoint connected regions remain internally connected when any of their boundary edges are deleted. Once all region boundaries are deleted, each region is exactly one connected component and hence one quotient vertex. The degree of a quotient vertex is bounded by the original cut of its component, with equality when designated edges are bridges. These statements identify the path vertices to be suppressed and their exact degrees.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.induce_delete_region_cuts
{V ι : Type}
[Fintype V]
(B : SimpleGraph V)
(P : ι → Finset V)
(disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j))
(removed : Set (Sym2 V))
(subset : removed ⊆ ⋃ (i : ι), ↑(B.cutFinset (P i)))
(i : ι)
:
SimpleGraph.induce {v : V | v ∈ P i} (B.deleteEdges removed) = SimpleGraph.induce {v : V | v ∈ P i} B
theorem
Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.exists_region_component
{V ι : Type}
[Fintype V]
(B : SimpleGraph V)
(P : ι → Finset V)
(connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected)
(disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j))
(i : ι)
:
∃ (C : (B.deleteEdges (⋃ (j : ι), ↑(B.cutFinset (P j)))).ConnectedComponent), C.supp.toFinset = P i
theorem
Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.exists_region_embedding
{V ι : Type}
[Fintype V]
(B : SimpleGraph V)
(P : ι → Finset V)
(connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected)
(disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j))
:
∃ (f : ι ↪ (B.deleteEdges (⋃ (j : ι), ↑(B.cutFinset (P j)))).ConnectedComponent), ∀ (i : ι), (f i).supp.toFinset = P i
theorem
Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.ncard_neighborSet_le_cut
{V : Type}
[Fintype V]
(B : SimpleGraph V)
(F : Set (Sym2 V))
(C : (B.deleteEdges F).ConnectedComponent)
:
theorem
Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.ncard_neighborSet_eq_cut
{V : Type}
[Fintype V]
(B : SimpleGraph V)
(F : Set (Sym2 V))
(bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e)
(C : (B.deleteEdges F).ConnectedComponent)
: