Connectivity and acyclicity of bridge quotients

Walks project to the component quotient and quotient walks lift through the connected contracted pieces. An original bridge remains a bridge in the quotient: a quotient path avoiding its image would lift to an original path avoiding the bridge. Thus contracting along the complement of a set of bridges produces a forest, and a tree when the original graph is connected.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.reachable_lift {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) {C D : (B.deleteEdges F).ConnectedComponent} (reachable : (graph B F).Reachable C D) {u v : V} (hu : u ∈ C.supp) (hv : v ∈ D.supp) : B.Reachable u v

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.reachable_project {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) {u v : V} (reachable : B.Reachable u v) : (graph B F).Reachable ((B.deleteEdges F).connectedComponentMk u) ((B.deleteEdges F).connectedComponentMk v)

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.reachable_iff {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) {C D : (B.deleteEdges F).ConnectedComponent} {u v : V} (hu : u ∈ C.supp) (hv : v ∈ D.supp) : (graph B F).Reachable C D ↔ B.Reachable u v

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.connected {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (original : B.Connected) : (graph B F).Connected

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.edge_image {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : Sym2.map (B.deleteEdges F).connectedComponentMk '' (F ∩ B.edgeSet) = (graph B F).edgeSet

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.edge_map_injOn {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : Set.InjOn (Sym2.map (B.deleteEdges F).connectedComponentMk) (F ∩ B.edgeSet)

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.edge_ncard {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).edgeSet.ncard = (F ∩ B.edgeSet).ncard

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.isBridge_of_adj {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) {C D : (B.deleteEdges F).ConnectedComponent} (edge : (graph B F).Adj C D) : (graph B F).IsBridge s(C, D)

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.isAcyclic {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).IsAcyclic

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.isTree {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (original : B.Connected) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).IsTree

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.component_isTree {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) (C : (graph B F).ConnectedComponent) : C.toSimpleGraph.IsTree

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.isBridge_of_mem_region_cut {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) {i : ι} {e : Sym2 V} (member : e ∈ B.cutFinset (P i)) : B.IsBridge e

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.ofRegions_isAcyclic {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) : (ofRegions B P).IsAcyclic

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.Internal.ofRegions_component_isTree {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) (C : (ofRegions B P).ConnectedComponent) : C.toSimpleGraph.IsTree