Common subdivision for finite transfer

This module proves step 1 of finite transfer. The part of the extension graph supported on the old source skeleton is extracted as a trace graph. It is a subdivision of the old skeleton and remains 2-connected. Its finitely many vertices are then inserted, one at a time, into both realizations of the generated pair. CellStructure.SubdivData.realizeHomeo transports every source subdivision parameter to the matching target edge.

The resulting theorem Schoenflies.commonSubdivision discharges the former Schoenflies.CommonSubdivision interface under the same infinite name-supply assumption used by the ear construction.

Blueprint

• Schoenflies.commonSubdivision — the common-subdivision part of step 1 in the proof of thm:finite-transfer(a).
• Schoenflies.finite_transfer_toward_square — thm:finite-transfer(a).
• Schoenflies.IsPlaneSubdivisionExtension.trace_isTwoConnected — the trace theorem for two arbitrary plane drawings, used when assembling target/mesh overlays.

theorem Graph.connected_of_isPreconnected_pointSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (hdraw : G.IsDrawing drawing) (hconn : IsPreconnected (G.pointSet drawing)) (hne : G.vertexSet.Nonempty) : G.Connected

A finite plane graph with nonempty, preconnected point set is combinatorially connected.

def Graph.traceGraph {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (A : Set Schoenflies.Plane) : Graph Schoenflies.Plane β

The part of a drawn graph supported on a prescribed set.

Equations

• G.traceGraph drawing A = (G.restrict {e : β | Graph.edgeArc drawing e ⊆ A}).induce (G.vertexSet ∩ A)

@[simp]

theorem Graph.traceGraph_vertexSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (A : Set Schoenflies.Plane) : (G.traceGraph drawing A).vertexSet = G.vertexSet ∩ A

The vertices retained by a trace graph.

@[simp]

theorem Graph.traceGraph_isLink {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {e : β} {x y : Schoenflies.Plane} (A : Set Schoenflies.Plane) : (G.traceGraph drawing A).IsLink e x y ↔ edgeArc drawing e ⊆ A ∧ G.IsLink e x y ∧ x ∈ A ∧ y ∈ A

A trace edge is exactly an ambient edge whose full arc and endpoints lie in the support.

theorem Graph.traceGraph_le {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (A : Set Schoenflies.Plane) : G.traceGraph drawing A ≤ G

A trace graph is a subgraph of its ambient graph.

theorem Graph.traceGraph_mono {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {A B : Set Schoenflies.Plane} (hAB : A ⊆ B) : G.traceGraph drawing A ≤ G.traceGraph drawing B

Enlarging the support enlarges the trace graph.

theorem Graph.pointSet_traceGraph_subset {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (A : Set Schoenflies.Plane) : (G.traceGraph drawing A).pointSet drawing ⊆ A

The trace graph occupies only its prescribed support.

theorem Graph.pointSet_traceGraph_eq {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (hdraw : G.IsDrawing drawing) (A : Set Schoenflies.Plane) (hsub : A ⊆ G.pointSet drawing) (habsorb : ∀ ⦃e : β⦄, e ∈ G.edgeSet → (edgeArc drawing e ∩ (A \ G.vertexSet)).Nonempty → edgeArc drawing e ⊆ A) : (G.traceGraph drawing A).pointSet drawing = A

An absorbed subset of a finite drawing is exactly the point set of its trace graph.

theorem Graph.IsDrawing.mem_walkVertices_of_mem_edgesCover_walk {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (hdraw : G.IsDrawing drawing) {u v z : Schoenflies.Plane} {W : List β} (hW : G.IsWalk u W v) (hzV : z ∈ G.vertexSet) (hz : z ∈ edgesCover drawing W) : z ∈ G.walkVertices u W

A graph vertex lying on a drawn walk is one of the walk's combinatorial vertices.

theorem Graph.IsTwoConnected.spanning_mono {α : Type u_2} {δ : Type u_3} {A B : Graph α δ} (hA : A.IsTwoConnected) (hAB : A ≤ B) (hV : B.vertexSet ⊆ A.vertexSet) : B.IsTwoConnected

Adding edges without adding vertices preserves 2-connectivity.

theorem Schoenflies.trace_absorb {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) ⦃f : γ⦄ : f ∈ H.edgeSet → (Graph.edgeArc Hdraw f ∩ (R.skeletonSet \ H.vertexSet)).Nonempty → Graph.edgeArc Hdraw f ⊆ R.skeletonSet

An extension edge meeting the interior of the old skeleton is absorbed by that skeleton.

theorem Schoenflies.trace_pointSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) : (H.traceGraph Hdraw R.skeletonSet).pointSet Hdraw = R.skeletonSet

The extension trace on the old skeleton occupies exactly the old skeleton.

theorem Schoenflies.edge_trace_pointSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {e : γ} (he : e ∈ S.skel.edgeSet) : (H.traceGraph Hdraw (Graph.edgeArc R.drawing e)).pointSet Hdraw = Graph.edgeArc R.drawing e

The trace supported on one old edge occupies that entire edge arc.

theorem Schoenflies.exists_edge_trace {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {e a b : γ} (hab : S.skel.IsLink e a b) : ∃ (D : List γ), H.IsPath (R.pos a) D (R.pos b) ∧ Graph.edgesCover Hdraw D = Graph.edgeArc R.drawing e

Every old edge is the drawn carrier of a path in the extension graph.

theorem Schoenflies.pathGraph_edge_trace_le {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {e a b : γ} (hab : S.skel.IsLink e a b) {D : List γ} (hD : H.IsPath (R.pos a) D (R.pos b)) (hcover : Graph.edgesCover Hdraw D = Graph.edgeArc R.drawing e) : H.pathGraphOf (R.pos a) D ≤ H.traceGraph Hdraw (Graph.edgeArc R.drawing e)

The path tracing an old edge is contained in the trace supported on that edge.

theorem Schoenflies.old_vertex_mem_trace {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {a : γ} (ha : a ∈ S.skel.vertexSet) : R.pos a ∈ (H.traceGraph Hdraw R.skeletonSet).vertexSet

Every old skeleton vertex belongs to the full skeleton trace.

theorem Schoenflies.reaches_trace_of_isWalk {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {a b : γ} {W : List γ} (hW : S.skel.IsWalk a W b) : (H.traceGraph Hdraw R.skeletonSet).Reaches (R.pos a) (R.pos b)

An old skeleton walk expands to a reachability witness in the extension trace.

theorem Schoenflies.old_vertices_reach_trace {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) (hR2 : R.graph.IsTwoConnected) {a b : γ} (ha : a ∈ S.skel.vertexSet) (hb : b ∈ S.skel.vertexSet) : (H.traceGraph Hdraw R.skeletonSet).Reaches (R.pos a) (R.pos b)

Any two old vertices are joined inside the extension trace.

theorem Schoenflies.exists_reaches_old_vertex {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {x : Plane} (hx : x ∈ (H.traceGraph Hdraw R.skeletonSet).vertexSet) : ∃ a ∈ S.skel.vertexSet, (H.traceGraph Hdraw R.skeletonSet).Reaches x (R.pos a)

Every trace vertex reaches an old skeleton vertex.

theorem Schoenflies.exists_reaches_old_vertex_delete {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {c x : Plane} (hx : x ∈ (H.traceGraph Hdraw R.skeletonSet).vertexSet) (hxc : x ≠ c) : ∃ a ∈ S.skel.vertexSet, ((H.traceGraph Hdraw R.skeletonSet).deleteVerts {c}).Reaches x (R.pos a)

After deleting a distinct trace vertex, every remaining vertex still reaches an old one.

theorem Schoenflies.reaches_trace_delete_of_deleteVerts_isWalk {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {z a b : γ} {W : List γ} (hzS : z ∈ S.skel.vertexSet) (hW : (S.skel.deleteVerts {z}).IsWalk a W b) : ((H.traceGraph Hdraw R.skeletonSet).deleteVerts {R.pos z}).Reaches (R.pos a) (R.pos b)

An old walk avoiding a vertex expands to a trace walk avoiding its realized point.

theorem Schoenflies.reaches_trace_delete_of_deleteEdges_isWalk {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) {c : Plane} (hcold : c ∉ R.graph.vertexSet) {e₀ : γ} (he₀ : e₀ ∈ S.skel.edgeSet) (hce₀ : c ∈ Graph.edgeArc R.drawing e₀) {a b : γ} {W : List γ} (hW : (S.skel.deleteEdges {e₀}).IsWalk a W b) : ((H.traceGraph Hdraw R.skeletonSet).deleteVerts {c}).Reaches (R.pos a) (R.pos b)

An old walk avoiding an edge expands to a trace walk avoiding an interior point of it.

theorem Schoenflies.trace_isTwoConnected {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension R outer dom H Hdraw) (hR2 : R.graph.IsTwoConnected) : (H.traceGraph Hdraw R.skeletonSet).IsTwoConnected

The part of an extension graph supported on a 2-connected old skeleton is 2-connected.

Traces of arbitrary plane subdivisions

The preceding result is phrased for a realized cell structure because that is the interface used by finite transfer. Overlay assembly also needs the same fact for an ordinary plane graph, notably the anchored square mesh. The proof only uses the local subdivision data recorded below; in particular it does not use 2-connectivity of the ambient graph.

structure Schoenflies.IsPlaneSubdivisionExtension {β : Type u_2} {δ : Type u_3} (G : Graph Plane β) (Gdraw : β → ℝ → Plane) (K : Graph Plane δ) (Kdraw : δ → ℝ → Plane) : Prop

The local data saying that K contains an edge subdivision of the drawn plane graph G. Crossings with other parts of K are allowed at vertices of K.

• finite : K.Finite

  The ambient graph is finite.

• oldIsDrawing : G.IsDrawing Gdraw

  The old graph is drawn in the plane.

• isDrawing : K.IsDrawing Kdraw

  The ambient graph is drawn in the plane.

• vertexSet_subset : G.vertexSet ⊆ K.vertexSet

  Every old vertex is an ambient vertex.

• pointSet_subset : G.pointSet Gdraw ⊆ K.pointSet Kdraw

  The old carrier lies in the ambient carrier.

• edge_subset ⦃e : β⦄ : e ∈ G.edgeSet → ∀ ⦃f : δ⦄, f ∈ K.edgeSet → (Graph.edgeArc Kdraw f ∩ (Graph.edgeArc Gdraw e \ K.vertexSet)).Nonempty → Graph.edgeArc Kdraw f ⊆ Graph.edgeArc Gdraw e

  An ambient edge meeting an old edge away from ambient vertices is contained in that old edge.

theorem Schoenflies.IsPlaneSubdivisionExtension.trace_absorb {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) ⦃f : δ⦄ : f ∈ K.edgeSet → (Graph.edgeArc Kdraw f ∩ (G.pointSet Gdraw \ K.vertexSet)).Nonempty → Graph.edgeArc Kdraw f ⊆ G.pointSet Gdraw

An ambient edge meeting the old carrier away from ambient vertices is absorbed by it.

theorem Schoenflies.IsPlaneSubdivisionExtension.trace_pointSet {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) : (K.traceGraph Kdraw (G.pointSet Gdraw)).pointSet Kdraw = G.pointSet Gdraw

The trace on the old carrier occupies exactly that carrier.

theorem Schoenflies.IsPlaneSubdivisionExtension.edge_trace_pointSet {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {e : β} (he : e ∈ G.edgeSet) : (K.traceGraph Kdraw (Graph.edgeArc Gdraw e)).pointSet Kdraw = Graph.edgeArc Gdraw e

The trace supported on one old edge occupies the entire old edge.

theorem Schoenflies.IsPlaneSubdivisionExtension.exists_edge_trace {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {e : β} {a b : Plane} (hab : G.IsLink e a b) : ∃ (D : List δ), K.IsPath a D b ∧ Graph.edgesCover Kdraw D = Graph.edgeArc Gdraw e

Every old edge is the carrier of an ambient path.

theorem Schoenflies.IsPlaneSubdivisionExtension.pathGraph_edge_trace_le {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {e : β} {a b : Plane} (hab : G.IsLink e a b) {D : List δ} (hD : K.IsPath a D b) (hcover : Graph.edgesCover Kdraw D = Graph.edgeArc Gdraw e) : K.pathGraphOf a D ≤ K.traceGraph Kdraw (Graph.edgeArc Gdraw e)

The path tracing an old edge lies in the trace supported on that edge.

theorem Schoenflies.IsPlaneSubdivisionExtension.old_vertex_mem_trace {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {a : Plane} (ha : a ∈ G.vertexSet) : a ∈ (K.traceGraph Kdraw (G.pointSet Gdraw)).vertexSet

Every old vertex belongs to the full old-carrier trace.

theorem Schoenflies.IsPlaneSubdivisionExtension.reaches_trace_of_isWalk {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {a b : Plane} {W : List β} (hW : G.IsWalk a W b) : (K.traceGraph Kdraw (G.pointSet Gdraw)).Reaches a b

An old walk expands to reachability in the ambient trace.

theorem Schoenflies.IsPlaneSubdivisionExtension.old_vertices_reach_trace {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) (hG2 : G.IsTwoConnected) {a b : Plane} (ha : a ∈ G.vertexSet) (hb : b ∈ G.vertexSet) : (K.traceGraph Kdraw (G.pointSet Gdraw)).Reaches a b

Any two old vertices are joined inside the ambient trace.

theorem Schoenflies.IsPlaneSubdivisionExtension.exists_reaches_old_vertex {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {x : Plane} (hx : x ∈ (K.traceGraph Kdraw (G.pointSet Gdraw)).vertexSet) : ∃ a ∈ G.vertexSet, (K.traceGraph Kdraw (G.pointSet Gdraw)).Reaches x a

Every trace vertex reaches an old vertex.

theorem Schoenflies.IsPlaneSubdivisionExtension.exists_reaches_old_vertex_delete {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {c x : Plane} (hx : x ∈ (K.traceGraph Kdraw (G.pointSet Gdraw)).vertexSet) (hxc : x ≠ c) : ∃ a ∈ G.vertexSet, ((K.traceGraph Kdraw (G.pointSet Gdraw)).deleteVerts {c}).Reaches x a

After deleting a distinct trace vertex, every remaining vertex still reaches an old one.

theorem Schoenflies.IsPlaneSubdivisionExtension.reaches_trace_delete_of_deleteVerts_isWalk {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {z a b : Plane} {W : List β} (hzG : z ∈ G.vertexSet) (hW : (G.deleteVerts {z}).IsWalk a W b) : ((K.traceGraph Kdraw (G.pointSet Gdraw)).deleteVerts {z}).Reaches a b

An old walk avoiding a vertex expands to a trace walk avoiding that vertex.

theorem Schoenflies.IsPlaneSubdivisionExtension.reaches_trace_delete_of_deleteEdges_isWalk {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) {c : Plane} (hcold : c ∉ G.vertexSet) {e₀ : β} (he₀ : e₀ ∈ G.edgeSet) (hce₀ : c ∈ Graph.edgeArc Gdraw e₀) {a b : Plane} {W : List β} (hW : (G.deleteEdges {e₀}).IsWalk a W b) : ((K.traceGraph Kdraw (G.pointSet Gdraw)).deleteVerts {c}).Reaches a b

An old walk avoiding an edge expands to a trace walk avoiding an interior point of it.

theorem Schoenflies.IsPlaneSubdivisionExtension.trace_isTwoConnected {β : Type u_2} {δ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {K : Graph Plane δ} {Kdraw : δ → ℝ → Plane} (h : IsPlaneSubdivisionExtension G Gdraw K Kdraw) (hG2 : G.IsTwoConnected) : (K.traceGraph Kdraw (G.pointSet Gdraw)).IsTwoConnected

The part of an ambient plane graph supported on a 2-connected old graph is 2-connected. No connectivity assumption on the ambient graph is needed.

theorem Schoenflies.CellStructure.exists_substWalk_raw {γ : Type u_1} {S : CellStructure γ} {edge left right newEdge₁ newEdge₂ u v : γ} {W : List γ} (hl : S.skel.IsLink edge left right) (h : S.skel.IsWalk u W v) : ∃ (W' : List γ), S.SubstWalk edge left right newEdge₁ newEdge₂ u W W'

Replace every occurrence of a distinguished edge in a walk by its two-edge subdivision.

theorem Schoenflies.CellStructure.exists_subdivData {γ : Type u_1} {S : CellStructure γ} (hcycles : S.BoundaryCycles) {edge left right newVertex newEdge₁ newEdge₂ : γ} (hl : S.skel.IsLink edge left right) (hv : newVertex ∉ S.cells) (he₁ : newEdge₁ ∉ S.cells) (he₂ : newEdge₂ ∉ S.cells) (hv₁ : newVertex ≠ newEdge₁) (hv₂ : newVertex ≠ newEdge₂) (he₁₂ : newEdge₁ ≠ newEdge₂) : ∃ (d : S.SubdivData), d.edge = edge ∧ d.left = left ∧ d.right = right ∧ d.newVertex = newVertex ∧ d.newEdge₁ = newEdge₁ ∧ d.newEdge₂ = newEdge₂

Build subdivision data for an edge from three pairwise distinct fresh cell names.

theorem Schoenflies.CellStructure.SubdivData.skeleton_isTwoConnected {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} (hS2 : S.skel.IsTwoConnected) (hlr : d.left ≠ d.right) : d.skeleton.IsTwoConnected

Subdividing one edge of a 2-connected skeleton preserves 2-connectivity.

theorem Schoenflies.CellStructure.SubdivData.outerSet_realize {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (d.realize R t ht).outerSet = R.outerSet

A geometric edge subdivision leaves the realized outer set unchanged.

theorem Schoenflies.CellStructure.SubdivData.old_notMem_outer {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {f : γ} (hfe : f ≠ d.edge) (hnew : f ∉ d.outer.edgeSet) : f ∉ S.outerGraph.edgeSet

An unchanged old edge is outer after subdivision only if it was outer before subdivision.

theorem Schoenflies.CellStructure.SubdivData.edge_notMem_outer_of_newEdge₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} (hnew : d.newEdge₁ ∉ d.outer.edgeSet) : d.edge ∉ S.outerGraph.edgeSet

If the first half of the subdivided edge is not outer, neither was the original edge.

theorem Schoenflies.CellStructure.SubdivData.edge_notMem_outer_of_newEdge₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} (hnew : d.newEdge₂ ∉ d.outer.edgeSet) : d.edge ∉ S.outerGraph.edgeSet

If the second half of the subdivided edge is not outer, neither was the original edge.

theorem Schoenflies.CellStructure.SubdivData.isWeaklyAdmissible_realize {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {outer dom : Set Plane} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hR : R.IsWeaklyAdmissible outer dom) : (d.realize R t ht).IsWeaklyAdmissible outer dom

Realizing an interior edge subdivision preserves weak admissibility.

noncomputable def Schoenflies.GeneratedPair.subdivide {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (d : P.str.SubdivData) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

Subdivide a generated matched pair at corresponding source and target parameters.

Equations

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

@[simp]

theorem Schoenflies.GeneratedPair.subdivide_src {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (d : P.str.SubdivData) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (P.subdivide d ht).src = d.realize P.src t ht

The source realization of a subdivided pair is the source subdivision.

@[simp]

theorem Schoenflies.GeneratedPair.subdivide_tgt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (d : P.str.SubdivData) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : (P.subdivide d ht).tgt = d.realize P.tgt (d.targetParam P.homeo t) ⋯

The target realization uses the parameter transported by the skeleton homeomorphism.

structure Schoenflies.GeneratedPair.SubdivideAtData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (p : Plane) : Type u_1

The output of inserting one source skeleton point into a matched generated pair.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The pair after the possible subdivision.

• parent : γ → γ

  The new-to-old cell parent map.

• refines_src : self.pair.src.Refines P.src self.parent

  Source refinement along parent.

• refines_tgt : self.pair.tgt.Refines P.tgt self.parent

  Target refinement along the same parent.

• skeletonSet_eq : self.pair.src.skeletonSet = P.src.skeletonSet

  Subdivision does not change the occupied source skeleton.

• targetSkeletonSet_eq : self.pair.tgt.skeletonSet = P.tgt.skeletonSet

  Subdivision does not change the occupied target skeleton.

• homeo_eqOn : Set.EqOn self.pair.homeo.toFun P.homeo.toFun P.src.skeletonSet

  The transported skeleton map is the old map as a point map.

• vertexSet_eq : self.pair.src.graph.vertexSet = insert p P.src.graph.vertexSet

  The requested point and every old vertex are vertices of the new source graph.

• targetVertexSet_eq : self.pair.tgt.graph.vertexSet = insert (P.homeo.toFun p) P.tgt.graph.vertexSet

  The corresponding target point and every old target vertex are vertices as well.

theorem Schoenflies.GeneratedPair.exists_subdivideAtData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {p : Plane} (hp : p ∈ P.src.skeletonSet) : Nonempty (P.SubdivideAtData p)

Every point of the source skeleton can be made a vertex by one matched subdivision.

structure Schoenflies.GeneratedPair.SubdivideTargetAtData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (p : Plane) : Type u_1

The output of inserting one target skeleton point into a matched generated pair.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The pair after the possible subdivision.

• parent : γ → γ

  The new-to-old cell parent map.

• refines_src : self.pair.src.Refines P.src self.parent

  Source refinement along parent.

• refines_tgt : self.pair.tgt.Refines P.tgt self.parent

  Target refinement along the same parent.

• sourceSkeletonSet_eq : self.pair.src.skeletonSet = P.src.skeletonSet

  The occupied source skeleton is unchanged.

• skeletonSet_eq : self.pair.tgt.skeletonSet = P.tgt.skeletonSet

  The occupied target skeleton is unchanged.

• homeo_eqOn : Set.EqOn self.pair.homeo.toFun P.homeo.toFun P.src.skeletonSet

  The transported skeleton map agrees with the old one.

• vertexSet_eq : self.pair.tgt.graph.vertexSet = insert p P.tgt.graph.vertexSet

  The requested point and every old vertex are target vertices of the new pair.

theorem Schoenflies.GeneratedPair.exists_subdivideTargetAtData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {p : Plane} (hp : p ∈ P.tgt.skeletonSet) : Nonempty (P.SubdivideTargetAtData p)

Every target skeleton point can be made a vertex by one matched subdivision.

structure Schoenflies.GeneratedPair.SubdivideSetData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (s : Set Plane) : Type u_1

The output of inserting a finite set of source skeleton points.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The pair after all subdivisions.

• parent : γ → γ

  The composite new-to-old cell parent map.

• refines_src : self.pair.src.Refines P.src self.parent

  Source refinement along parent.

• refines_tgt : self.pair.tgt.Refines P.tgt self.parent

  Target refinement along the same parent.

• skeletonSet_eq : self.pair.src.skeletonSet = P.src.skeletonSet

  Subdivision does not change the occupied source skeleton.

• homeo_eqOn : Set.EqOn self.pair.homeo.toFun P.homeo.toFun P.src.skeletonSet

  The transported skeleton map agrees with the old one on that unchanged skeleton.

• vertexSet_subset : s ⊆ self.pair.src.graph.vertexSet

  Every requested point is a vertex of the final source graph.

theorem Schoenflies.GeneratedPair.exists_subdivideSetData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {s : Set Plane} (hs : s.Finite) (hsub : s ⊆ P.src.skeletonSet) : Nonempty (P.SubdivideSetData s)

Every finite set of source skeleton points can simultaneously be made vertices.

structure Schoenflies.GeneratedPair.SubdivideTargetSetData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (s : Set Plane) : Type u_1

The output of inserting a finite set of target skeleton points.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The pair after all subdivisions.

• parent : γ → γ

  The composite new-to-old cell parent map.

• refines_src : self.pair.src.Refines P.src self.parent

  Source refinement along parent.

• refines_tgt : self.pair.tgt.Refines P.tgt self.parent

  Target refinement along the same parent.

• sourceSkeletonSet_eq : self.pair.src.skeletonSet = P.src.skeletonSet

  The occupied source skeleton is unchanged.

• skeletonSet_eq : self.pair.tgt.skeletonSet = P.tgt.skeletonSet

  The occupied target skeleton is unchanged.

• homeo_eqOn : Set.EqOn self.pair.homeo.toFun P.homeo.toFun P.src.skeletonSet

  The final skeleton map agrees with the original one on the original source skeleton.

• vertexSet_subset : s ⊆ self.pair.tgt.graph.vertexSet

  Every requested point is a vertex of the final target graph.

theorem Schoenflies.GeneratedPair.exists_subdivideTargetSetData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {s : Set Plane} (hs : s.Finite) (hsub : s ⊆ P.tgt.skeletonSet) : Nonempty (P.SubdivideTargetSetData s)

Every finite set of target skeleton points can simultaneously be made vertices.

structure Schoenflies.CommonSubdivisionData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Type u_1

Explicit output data for the common-subdivision construction.

• graph : Graph Plane γ

  The part of H supported on the old source skeleton.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The matched pair after inserting every vertex of graph.

• parent : γ → γ

  The composite parent map from the subdivided pair to P.

• graph_isTwoConnected : self.graph.IsTwoConnected

  The traced graph remains 2-connected.

• graph_le : self.graph ≤ H

  The traced graph is a subgraph of the given extension.

• isPartialTransferOf : IsPartialTransferOf self.pair P self.graph Hdraw self.parent

  The refined pair realizes the traced graph and contains all of its vertices.

noncomputable def Schoenflies.commonSubdivisionData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.src srcOuter srcDom H Hdraw) : CommonSubdivisionData P H Hdraw

Construct the traced graph, matched subdivided pair, and their composite parent map.

Equations

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

theorem Schoenflies.commonSubdivision {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.src srcOuter srcDom H Hdraw) : CommonSubdivision P H Hdraw

Step 1 of finite transfer: construct the common matched subdivision.

theorem Schoenflies.transfer_of_ears {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.src srcOuter srcDom H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsPartialTransferOf T P H Hdraw par

Steps 1–3 of finite transfer, with the common subdivision and every ear constructed.

theorem Schoenflies.finite_transfer_toward_square {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.src srcOuter srcDom H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTransferOf T P H Hdraw par

thm:finite-transfer, direction (a).