Restricting a one-vertex cut through another cut

When the left side of a second cut lies in the right factor of a first cut, the second cut restricts to that factor. This is the elementary nesting step needed to display successive wedge factors without making any assumptions on their origin.

theorem Utilities.Certificate.CoreVertexCut.Data.leftVertices_subset_rightVertices_of_left_subset_right {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (first second : Data spec.core) (hSubset : second.left ⊆ first.right) : leftVertices spec second ⊆ rightVertices spec first

Core-side nesting lifts uniformly through every positive subdivision. If the second finite left side lies in the first finite right side, every subdivision vertex belonging to the second left factor lies in the first right factor.

noncomputable def Utilities.OneVertexCut.restrictRight {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) : OneVertexCut first.rightGraph

The second cut may be viewed inside the right factor of the first when its left side is contained in that factor.

Equations

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

theorem Utilities.OneVertexCut.restrictRight_graph_connected_factors {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) (hK : graphConnected K) : graphConnected (first.restrictRight second hLeft).leftGraph ∧ graphConnected (first.restrictRight second hLeft).rightGraph

Connectivity of the restricted-cut factors follows from connectivity of the original ambient graph.

def Utilities.OneVertexCut.restrictRightLeftVertex {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) (vertex : (first.restrictRight second hLeft).leftGraph.V) : second.leftGraph.V

Flatten the two subtype layers of the restricted left factor.

Equations

• first.restrictRightLeftVertex second hLeft vertex = ⟨↑↑vertex, ⋯⟩

@[simp]

theorem Utilities.OneVertexCut.restrictRightLeftVertex_val {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) (vertex : (first.restrictRight second hLeft).leftGraph.V) : ↑(first.restrictRightLeftVertex second hLeft vertex) = ↑↑vertex

theorem Utilities.OneVertexCut.restrictRightLeftVertex_bijective {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) : Function.Bijective (first.restrictRightLeftVertex second hLeft)

noncomputable def Utilities.OneVertexCut.restrictRightLeftIso {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) : CFGraphIso (first.restrictRight second hLeft).leftGraph second.leftGraph

Flatten the left factor of a restricted cut back to the second cut's original left factor. This removes the two layers of induced-subgraph subtypes without changing any edge multiplicity.

Equations

• first.restrictRightLeftIso second hLeft = { vertexEquiv := Equiv.ofBijective (first.restrictRightLeftVertex second hLeft) ⋯, map_num_edges := ⋯ }

@[simp]

theorem Utilities.OneVertexCut.restrictRightLeftIso_apply_leftGlue {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) : (first.restrictRightLeftIso second hLeft).vertexEquiv (first.restrictRight second hLeft).leftGlue = second.leftGlue

theorem Utilities.OneVertexCut.genus_eq_nested_restrictRight {K : CFGraph} (first second : OneVertexCut K) (hLeft : second.left ⊆ first.right) : K.genus = first.leftGraph.genus + (first.restrictRight second hLeft).leftGraph.genus + (first.restrictRight second hLeft).rightGraph.genus

The two successive cuts decompose the genus into the first left factor and the two factors of the restricted second cut.