Presentations by one separating bridge

OneBridgeCut is occurrence-safe finite data exhibiting an ambient graph as two induced vertex-disjoint factors joined by one specified bridge occurrence. The cross-edge equation is phrased with numEdges, so parallel edges inside either factor remain fully visible while the separating edge has multiplicity exactly one.

structure MarkedGraphs.OneBridgeCut (K : CFGraph) : Type u

A finite presentation of K as two induced pieces joined by a single unit bridge.

• left : Finset K.V

  The nonempty left side of the vertex partition separated from the right side by exactly one bridge occurrence.

• right : Finset K.V

  The nonempty right side of the disjoint vertex partition separated by the bridge.

• leftAttach : K.V

  The bridge endpoint belonging to the left side.

• rightAttach : K.V

  The bridge endpoint belonging to the right side.

• left_nonempty : self.left.Nonempty
• right_nonempty : self.right.Nonempty
• leftAttach_mem : self.leftAttach ∈ self.left
• rightAttach_mem : self.rightAttach ∈ self.right
• disjoint : Disjoint self.left self.right
• vertex_cover (z : K.V) : z ∈ self.left ∨ z ∈ self.right
• cross_num_edges (a b : K.V) : a ∈ self.left → b ∈ self.right → numEdges K a b = if a = self.leftAttach ∧ b = self.rightAttach then 1 else 0

@[reducible, inline]

noncomputable abbrev MarkedGraphs.OneBridgeCut.leftGraph {K : CFGraph} (cut : OneBridgeCut K) : CFGraph

The induced left factor.

Equations

• cut.leftGraph = Utilities.inducedSubgraph K cut.left ⋯

@[reducible, inline]

noncomputable abbrev MarkedGraphs.OneBridgeCut.rightGraph {K : CFGraph} (cut : OneBridgeCut K) : CFGraph

The induced right factor.

Equations

• cut.rightGraph = Utilities.inducedSubgraph K cut.right ⋯

noncomputable def MarkedGraphs.OneBridgeCut.leftGlue {K : CFGraph} (cut : OneBridgeCut K) : cut.leftGraph.V

The left endpoint, as a vertex of the left induced factor.

Equations

• cut.leftGlue = ⟨cut.leftAttach, ⋯⟩

noncomputable def MarkedGraphs.OneBridgeCut.rightGlue {K : CFGraph} (cut : OneBridgeCut K) : cut.rightGraph.V

The right endpoint, as a vertex of the right induced factor.

Equations

• cut.rightGlue = ⟨cut.rightAttach, ⋯⟩

@[simp]

theorem MarkedGraphs.OneBridgeCut.leftGlue_val {K : CFGraph} (cut : OneBridgeCut K) : ↑cut.leftGlue = cut.leftAttach

@[simp]

theorem MarkedGraphs.OneBridgeCut.rightGlue_val {K : CFGraph} (cut : OneBridgeCut K) : ↑cut.rightGlue = cut.rightAttach

@[reducible, inline]

noncomputable abbrev MarkedGraphs.OneBridgeCut.bridgeGraph {K : CFGraph} (cut : OneBridgeCut K) : CFGraph

The concrete bridge graph determined by the cut.

Equations

• cut.bridgeGraph = Utilities.bridgeGraph cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue

noncomputable def MarkedGraphs.OneBridgeCut.vertexEquiv {K : CFGraph} (cut : OneBridgeCut K) : cut.bridgeGraph.V ≃ K.V

The vertex equivalence from the concrete bridge model to the ambient graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MarkedGraphs.OneBridgeCut.vertexEquiv_apply_left {K : CFGraph} (cut : OneBridgeCut K) (a : cut.leftGraph.V) : cut.vertexEquiv (Sum.inl a) = ↑a

@[simp]

theorem MarkedGraphs.OneBridgeCut.vertexEquiv_apply_right {K : CFGraph} (cut : OneBridgeCut K) (b : cut.rightGraph.V) : cut.vertexEquiv (Sum.inr b) = ↑b

noncomputable def MarkedGraphs.OneBridgeCut.graphIso {K : CFGraph} (cut : OneBridgeCut K) : Utilities.CFGraphIso cut.bridgeGraph K

The occurrence-safe isomorphism from the bridge model to the ambient graph.

Equations

• cut.graphIso = { vertexEquiv := cut.vertexEquiv, map_num_edges := ⋯ }

noncomputable def MarkedGraphs.OneBridgeCut.laplacianEquiv {K : CFGraph} (cut : OneBridgeCut K) : Utilities.Certificate.LaplacianEquiv cut.bridgeGraph K

The Laplacian equivalence supplied by a bridge cut.

Equations

• cut.laplacianEquiv = cut.graphIso.toLaplacianEquiv

theorem MarkedGraphs.OneBridgeCut.genus_eq {K : CFGraph} (cut : OneBridgeCut K) : K.genus = cut.leftGraph.genus + cut.rightGraph.genus

Genus is additive across a separating bridge.

theorem MarkedGraphs.OneBridgeCut.graph_connected_left_of_connected {K : CFGraph} (cut : OneBridgeCut K) (hK : graphConnected K) : graphConnected cut.leftGraph

A connected ambient graph has connected induced left factor across a single separating bridge.

def MarkedGraphs.OneBridgeCut.swap {K : CFGraph} (cut : OneBridgeCut K) : OneBridgeCut K

Exchange the two sides of a bridge cut.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MarkedGraphs.OneBridgeCut.swap_leftGraph {K : CFGraph} (cut : OneBridgeCut K) : cut.swap.leftGraph = cut.rightGraph

@[simp]

theorem MarkedGraphs.OneBridgeCut.swap_rightGraph {K : CFGraph} (cut : OneBridgeCut K) : cut.swap.rightGraph = cut.leftGraph

@[simp]

theorem MarkedGraphs.OneBridgeCut.swap_leftGlue {K : CFGraph} (cut : OneBridgeCut K) : cut.swap.leftGlue = cut.rightGlue

@[simp]

theorem MarkedGraphs.OneBridgeCut.swap_rightGlue {K : CFGraph} (cut : OneBridgeCut K) : cut.swap.rightGlue = cut.leftGlue

theorem MarkedGraphs.OneBridgeCut.graph_connected_right_of_connected {K : CFGraph} (cut : OneBridgeCut K) (hK : graphConnected K) : graphConnected cut.rightGraph

A connected ambient graph has connected induced right factor across a single separating bridge.

theorem MarkedGraphs.OneBridgeCut.graph_connected_factors_of_connected {K : CFGraph} (cut : OneBridgeCut K) (hK : graphConnected K) : graphConnected cut.leftGraph ∧ graphConnected cut.rightGraph

theorem MarkedGraphs.OneBridgeCut.graph_connected_of_factors {K : CFGraph} (cut : OneBridgeCut K) (hLeft : graphConnected cut.leftGraph) (hRight : graphConnected cut.rightGraph) : graphConnected K

Connected factors reconstruct a connected ambient graph.

theorem MarkedGraphs.OneBridgeCut.graph_connected_iff_factors {K : CFGraph} (cut : OneBridgeCut K) : graphConnected K ↔ graphConnected cut.leftGraph ∧ graphConnected cut.rightGraph