Realizing a 2-cell split

Schoenflies/CellulationInvariants.lean proves the step theorems of the second elementary operation: given a realization R' of S.splitFace d standing in the relation SplitData.IsCrosscutSplit to a realization R of S, the two invariants of lem:cellulation-invariants propagate. Nothing built such an R'. This module does.

Blueprint

• def:generated-structure, operation 2 — the 2-cell split whose realization is constructed here.
• lem:cellulation-invariants (i), (vii) — the invariants that SplitData.IsCrosscutSplit.isCellDecomposition_and_isFaceJordan derives from the output of this module.
• thm:general-crosscut (Schoenflies.crosscut_theorem) — what turns the constructed ear into the two new open 2-cells; it is applied inside IsCrosscutSplit.isRefinement, and this module supplies its hypotheses.

What is constructed

• Schoenflies.CellStructure.SplitData.EarCrosscut — the geometric input: an assignment of points to the ear's vertices and of parametrizations to the ear's edges, drawing the ear as a polygonal crosscut of the realized open 2-cell.
• Schoenflies.CellStructure.SplitData.realize — the realization of S.splitFace d built from R and such an ear. It is a def with lemmas, not an existential: splitPos, splitDrawing, splitCell are its three components, each with its own reduction lemmas (splitCell_face₁, splitCell_of_mem_cells, splitCell_earVertex, splitCell_earEdge, …), and realize_pos / realize_drawing / realize_cell connect them to the record.
• Schoenflies.CellStructure.SplitData.isCrosscutSplit_realize — the constructed realization stands in the relation IsCrosscutSplit to R. Composed with IsCrosscutSplit.isCellDecomposition_and_isFaceJordan this is the full induction step.

What is assumed, and who discharges it

realize itself asks only for EarCrosscut, whose six fields — pos_source, pos_target, injOn, isDrawing, subset_face, polygonal — say that the ear is drawn as a simple polygonal arc from R.pos d.source to R.pos d.target whose interior lies in the open 2-cell, plus the seventh, disjoint_skeleton, which is a fact about R alone and is discharged by Realization.disjoint_cell_skeletonSet from assertion (i). A producer that starts from Schoenflies.exists_crosscut_of_polyAccessible — a polygonal arc inside the face with both ends on its boundary — and cuts that arc into the ear's edges has all seven in hand.

isCrosscutSplit_realize asks in addition only for R.IsCellDecomposition D and R.IsFaceJordan.

It used to ask for a third thing — that the two boundary paths of the split 2-cell share nothing but their two ends — because SplitData did not imply it: its field paths_disjoint forbade the two paths a common edge but said nothing about a common interior vertex, and with a common interior vertex the two realized paths meet in a third point, so the IsCutPair clause of IsCrosscutSplit is false. That gap has since been closed at the source: SplitData now carries paths_meet and derives paths_disjoint from it. What follows is the record of a condition that producer of the SplitData chooses them (as the two arcs of one boundary cycle) and so can supply it. If a later wave prefers it as a field of SplitData, that is the right place for it.

The general lemmas this needed

Three facts about drawings and paths had no home on main and are proved here in the root Graph namespace. If a second consumer appears they belong in Schoenflies/Graph/:

• Graph.IsPath.map, Graph.walkVertices_map, Graph.IsPathGraph.map — a path pushes forward along an injective relabelling of the vertices. Graph.IsWalk.map was already on main (in Schoenflies/CombinatorialInvariance.lean); the path version needs the injectivity, because the freshness clause is a non-membership.
• Graph.IsDrawing.isArcBetween_walkPointSet — the point set of a drawn path is a simple arc between its two ends. This is the workhorse: it is what makes the realized ear an arc (so IsCrosscut applies) and what makes each realized boundary path an arc (so IsCutPair applies). The induction is on Graph.IsPath, and the freshness clause of a path is exactly what rules out the returning point that would break IsArcBetween.concatenate.

Pushing a path forward along a relabelling

theorem Graph.coveredVertices_map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {W : List β} (f : α → α') : (map f G).coveredVertices W = f '' G.coveredVertices W

theorem Graph.walkVertices_map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} (f : α → α') (u : α) (W : List β) : (map f G).walkVertices (f u) W = f '' G.walkVertices u W

theorem Graph.IsPath.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} {u v : α} {W : List β} (hf : Set.InjOn f G.vertexSet) (h : G.IsPath u W v) : (Graph.map f G).IsPath (f u) W (f v)

A path pushes forward along an injective relabelling. Unlike Graph.IsWalk.map this needs the injectivity: the freshness clause is a non-membership, and only an injective map reflects it.

theorem Graph.map_union {α : Type u_1} {α' : Type u_2} {β : Type u_3} (G H : Graph α β) (f : α → α') : map f (G.union H) = (map f G).union (map f H)

Relabelling commutes with the union. Both sides resolve a shared edge name in favour of the left-hand graph, and Graph.map keeps the edge set, so the two resolutions agree.

theorem Graph.IsPathGraph.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {f : α → α'} {u v : α} {W : List β} {P : Graph α β} (hf : Set.InjOn f P.vertexSet) (h : P.IsPathGraph u W v) : (Graph.map f P).IsPathGraph (f u) W (f v)

The point set of a drawn path

Graph.pointSet reads the vertex set and the edge set of a graph. Along a walk both are read off the list instead, and that is the form the induction below runs on.

def Graph.walkPointSet {β : Type u_1} (H : Graph Schoenflies.Plane β) (drw : β → ℝ → Schoenflies.Plane) (u : Schoenflies.Plane) (W : List β) : Set Schoenflies.Plane

The point set a walk occupies: the vertices it visits together with the arcs of its edges. For a path graph this is the whole of Graph.pointSet (walkPointSet_eq_pointSet).

Equations

• H.walkPointSet drw u W = H.walkVertices u W ∪ ⋃ e ∈ {e : β | e ∈ W}, Graph.edgeArc drw e

theorem Graph.walkPointSet_eq_pointSet {β : Type u_1} {H : Graph Schoenflies.Plane β} {drw : β → ℝ → Schoenflies.Plane} {u v : Schoenflies.Plane} {W : List β} (h : H.IsPathGraph u W v) : H.walkPointSet drw u W = H.pointSet drw

theorem Graph.walkPointSet_nil {β : Type u_1} {H : Graph Schoenflies.Plane β} {drw : β → ℝ → Schoenflies.Plane} (u : Schoenflies.Plane) : H.walkPointSet drw u [] = {u}

theorem Graph.walkPointSet_cons {β : Type u_1} {H : Graph Schoenflies.Plane β} {drw : β → ℝ → Schoenflies.Plane} (hD : H.IsDrawing drw) {e : β} {u w : Schoenflies.Plane} {W : List β} (hl : H.IsLink e u w) : H.walkPointSet drw u (e :: W) = edgeArc drw e ∪ H.walkPointSet drw w W

Peeling the first step off a walk peels its arc off the point set. The vertex the step departs from is an end of that arc, which is why nothing is left behind.

theorem Graph.IsDrawing.isArcBetween_walkPointSet {β : Type u_1} {H : Graph Schoenflies.Plane β} {drw : β → ℝ → Schoenflies.Plane} (hD : H.IsDrawing drw) {u v : Schoenflies.Plane} {W : List β} : H.IsPath u W v → u ≠ v → Schoenflies.IsArcBetween (H.walkPointSet drw u W) u v

The point set of a drawn path is a simple arc between its two ends.

The two pieces glued at each step are the arc of the first edge and the point set of the rest of the path, and IsArcBetween.concatenate asks that they meet only at the vertex between them. That is precisely the freshness clause of Graph.IsPath: the vertex the path departs from is not among those the rest of it visits, and every point the first arc shares with the rest of the drawing is a vertex the rest visits — a vertex by vertex_mem_edgeArc if it is one of the rest's vertices, and by edge_inter if it lies on one of the rest's arcs.

theorem Graph.IsDrawing.isArcBetween_pointSet {β : Type u_1} {H : Graph Schoenflies.Plane β} {drw : β → ℝ → Schoenflies.Plane} (hD : H.IsDrawing drw) {u v : Schoenflies.Plane} {W : List β} (h : H.IsPathGraph u W v) (huv : u ≠ v) : Schoenflies.IsArcBetween (H.pointSet drw) u v

What a realization does to a walk

Two facts about an existing realization, both of the shape "the realized cells of a piece of the skeleton occupy the point set that piece of the drawing occupies". They are what let the crosscut theorem, which speaks of point sets, be fed from the cell structure, which speaks of cells.

theorem Schoenflies.CellStructure.Realization.walkVertices_graph {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (u : γ) (W : List γ) : R.graph.walkVertices (R.pos u) W = R.pos '' S.skel.walkVertices u W

theorem Schoenflies.CellStructure.Realization.cellUnion_pathCells {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) : R.cellUnion (S.pathCells u W) = R.graph.walkPointSet R.drawing (R.pos u) W

The realized cells of a path occupy the point set the drawn path occupies. The two differ only in the endpoints an open 1-cell drops, and those are the points of the 0-cells the walk visits.

theorem Schoenflies.CellStructure.Realization.skeletonSet_subset_cellUnion {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.skeletonSet ⊆ R.cellUnion (S.skel.vertexSet ∪ S.skel.edgeSet)

The drawn skeleton is covered by the open cells of dimension 0 and 1.

theorem Schoenflies.CellStructure.Realization.disjoint_cell_skeletonSet {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) {D : Set Plane} (hcd : R.IsCellDecomposition D) {F : γ} (hF : F ∈ S.faces) : Disjoint (R.cell F) R.skeletonSet

An open 2-cell misses the drawn skeleton. Immediate from the disjointness clause of assertion (i): the skeleton is covered by cells of lower dimension.

The ear, drawn

SplitData fixes the abstract ear: a path graph d.ear glued to the skeleton at d.source and d.target. Drawing it means choosing a point for each of its vertices and a parametrization for each of its edges. EarCrosscut is the bundle of conditions under which that drawing is a polygonal crosscut of the realized open 2-cell R.cell d.face.

theorem Schoenflies.CellStructure.SplitData.source_mem_ear {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.source ∈ d.ear.vertexSet

theorem Schoenflies.CellStructure.SplitData.target_mem_ear {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.target ∈ d.ear.vertexSet

theorem Schoenflies.CellStructure.SplitData.source_mem_cells₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.source ∈ d.cells₂

theorem Schoenflies.CellStructure.SplitData.target_mem_cells₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.target ∈ d.cells₂

theorem Schoenflies.CellStructure.SplitData.subcells_face_diff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : S.subcells d.face \ {d.face} = d.cells₁ ∪ d.cells₂

The cells strictly below the split 2-cell are the cells of its two boundary paths. This is SplitData.sub_face read as a set identity; with assertion (i) it identifies the frontier of the old open 2-cell with the two realized boundary paths.

def Schoenflies.CellStructure.SplitData.earGraph {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (earPos : γ → Plane) : Graph Plane γ

The drawn ear: the abstract ear pushed into the plane along the chosen positions.

Equations

• d.earGraph earPos = Graph.map earPos d.ear

@[simp]

theorem Schoenflies.CellStructure.SplitData.vertexSet_earGraph {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (earPos : γ → Plane) : (d.earGraph earPos).vertexSet = earPos '' d.ear.vertexSet

@[simp]

theorem Schoenflies.CellStructure.SplitData.edgeSet_earGraph {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (earPos : γ → Plane) : (d.earGraph earPos).edgeSet = d.ear.edgeSet

def Schoenflies.CellStructure.SplitData.earSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (earPos : γ → Plane) (earDraw : γ → ℝ → Plane) : Set Plane

The point set the drawn ear occupies: the crosscut P of thm:general-crosscut.

Equations

• d.earSet earPos earDraw = (d.earGraph earPos).pointSet earDraw

structure Schoenflies.CellStructure.SplitData.EarCrosscut {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (earPos : γ → Plane) (earDraw : γ → ℝ → Plane) : Prop

The geometric input of one 2-cell split. A position for each vertex of the abstract ear and a parametrization for each of its edges, drawing the ear as a polygonal crosscut of the realized open 2-cell R.cell d.face.

Every clause is a statement about the ear's own drawing, and every one of them is what the finite-transfer module has in hand when it produces a crosscut from Schoenflies.exists_crosscut_of_polyAccessible: it starts from a simple polygonal arc P inside the face with its two ends on the boundary, and cuts P into the ear's edges.

• pos_source : earPos d.source = R.pos d.source

  The ear starts where the old 0-cell d.source sits.

• pos_target : earPos d.target = R.pos d.target

  …and ends where d.target sits.

• injOn : Set.InjOn earPos d.ear.vertexSet

  Distinct vertices of the ear are drawn at distinct points.

• isDrawing : (d.earGraph earPos).IsDrawing earDraw

  The ear is drawn as a plane graph.

• subset_face : d.earSet earPos earDraw \ {R.pos d.source, R.pos d.target} ⊆ R.cell d.face

  Every point of the drawn ear but its two ends is inside the old open 2-cell.

• disjoint_skeleton : Disjoint (R.cell d.face) R.skeletonSet

  The old open 2-cell misses the old drawn skeleton. This is a property of R alone, not of the ear; it is carried here so that the construction below depends on no ambient domain. Realization.disjoint_cell_skeletonSet discharges it from assertion (i).

• polygonal : IsPolygonal (d.earSet earPos earDraw)

  The drawn ear is polygonal.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.source_ne_target_pos {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : R.pos d.source ≠ R.pos d.target

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.mem_earSet_of_mem_ear {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} {z : γ} (hz : z ∈ d.ear.vertexSet) : earPos z ∈ d.earSet earPos earDraw

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.edgeArc_subset_earSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ d.ear.edgeSet) : Graph.edgeArc earDraw f ⊆ d.earSet earPos earDraw

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.earPos_eq {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {z : γ} (hz : z ∈ d.ear.vertexSet) (hz' : z ∈ S.skel.vertexSet) : earPos z = R.pos z

On the two ends — the only vertices the ear shares with the old skeleton — the ear's positions agree with the old ones.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.pos_source_mem_earSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : R.pos d.source ∈ d.earSet earPos earDraw

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.pos_target_mem_earSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : R.pos d.target ∈ d.earSet earPos earDraw

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.earPos_mem_cell_face {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {z : γ} (hz : z ∈ d.ear.vertexSet) (hs : z ≠ d.source) (ht : z ≠ d.target) : earPos z ∈ R.cell d.face

An interior vertex of the ear is drawn strictly inside the old open 2-cell.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.earSet_inter_skeletonSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : d.earSet earPos earDraw ∩ R.skeletonSet ⊆ {R.pos d.source, R.pos d.target}

The drawn ear meets the old skeleton exactly in its two ends. The interior of the ear is inside the open 2-cell, and an open 2-cell misses the drawn skeleton.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.edgeArc_diff {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {f a b : γ} (hl : d.ear.IsLink f a b) : Graph.edgeArc earDraw f \ earPos '' d.ear.vertexSet = Graph.edgeArc earDraw f \ {earPos a, earPos b}

An ear edge's arc meets the ear's vertices exactly at its own two ends, so dropping all of the ear's vertices from it is the same as dropping its own two ends. This is what makes the definition of the new open 1-cells independent of a choice of orientation.

The realization built from a drawn ear

noncomputable def Schoenflies.CellStructure.SplitData.splitPos {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (earPos : γ → Plane) : γ → Plane

Where the split puts each 0-cell: the ear's vertices go where the ear's drawing puts them, everything else stays. On the ear's two ends the two prescriptions agree.

Equations

• d.splitPos R earPos z = if z ∈ d.ear.vertexSet then earPos z else R.pos z

noncomputable def Schoenflies.CellStructure.SplitData.splitDrawing {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (earDraw : γ → ℝ → Plane) : γ → ℝ → Plane

How the split draws each 1-cell.

Equations

• d.splitDrawing R earDraw f = if f ∈ d.ear.edgeSet then earDraw f else R.drawing f

noncomputable def Schoenflies.CellStructure.SplitData.splitCell {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (earPos : γ → Plane) (earDraw : γ → ℝ → Plane) : γ → Set Plane

The point set of each open cell after the split: the two new 2-cells are the two sides of the crosscut, the ear's vertices and edges are their points and their open arcs, and every surviving cell keeps its old point set.

Equations

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

theorem Schoenflies.CellStructure.SplitData.splitPos_of_mem_ear {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {z : γ} (hz : z ∈ d.ear.vertexSet) : d.splitPos R earPos z = earPos z

theorem Schoenflies.CellStructure.SplitData.splitPos_of_notMem_ear {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {z : γ} (hz : z ∉ d.ear.vertexSet) : d.splitPos R earPos z = R.pos z

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.splitPos_eq {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {z : γ} (hz : z ∈ S.skel.vertexSet) : d.splitPos R earPos z = R.pos z

theorem Schoenflies.CellStructure.SplitData.splitDrawing_of_mem_ear {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ d.ear.edgeSet) : d.splitDrawing R earDraw f = earDraw f

theorem Schoenflies.CellStructure.SplitData.splitDrawing_of_mem_skel {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ S.skel.edgeSet) : d.splitDrawing R earDraw f = R.drawing f

theorem Schoenflies.CellStructure.SplitData.splitCell_face₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} : d.splitCell R earPos earDraw d.face₁ = inside (R.cellUnion d.cells₁ ∪ d.earSet earPos earDraw)

theorem Schoenflies.CellStructure.SplitData.splitCell_face₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} : d.splitCell R earPos earDraw d.face₂ = inside (R.cellUnion d.cells₂ ∪ d.earSet earPos earDraw)

theorem Schoenflies.CellStructure.SplitData.splitCell_of_mem_cells {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} {σ : γ} (hσ : σ ∈ S.cells) : d.splitCell R earPos earDraw σ = R.cell σ

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.splitCell_earVertex {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {z : γ} (hz : z ∈ d.ear.vertexSet) : d.splitCell R earPos earDraw z = {earPos z}

theorem Schoenflies.CellStructure.SplitData.splitCell_earEdge {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ d.ear.edgeSet) : d.splitCell R earPos earDraw f = Graph.edgeArc earDraw f \ earPos '' d.ear.vertexSet

theorem Schoenflies.CellStructure.SplitData.edgeArc_splitDrawing_of_mem_skel {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ S.skel.edgeSet) : Graph.edgeArc (d.splitDrawing R earDraw) f = Graph.edgeArc R.drawing f

theorem Schoenflies.CellStructure.SplitData.edgeArc_splitDrawing_of_mem_ear {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earDraw : γ → ℝ → Plane} {f : γ} (hf : f ∈ d.ear.edgeSet) : Graph.edgeArc (d.splitDrawing R earDraw) f = Graph.edgeArc earDraw f

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.splitGraph_eq {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : Graph.map (d.splitPos R earPos) (S.splitFace d).skel = R.graph.union (d.earGraph earPos)

The skeleton of the split structure, drawn: the old drawn skeleton with the drawn ear glued on.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.isDrawing_split {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (R.graph.union (d.earGraph earPos)).IsDrawing (d.splitDrawing R earDraw)

The old drawn skeleton with the drawn ear glued on is a plane graph. The three clauses of Graph.IsDrawing all reduce, on a mixed pair, to the same fact: the ear meets the old drawing only at its two ends, because its interior lies in an open 2-cell and an open 2-cell misses the drawn skeleton.

theorem Schoenflies.CellStructure.SplitData.frontier_cell_face {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {D : Set Plane} (hcd : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : frontier (R.cell d.face) = R.cellUnion d.cells₁ ∪ R.cellUnion d.cells₂

The frontier of the old open 2-cell is the union of its two realized boundary paths. SplitData.sub_face says which cells lie below the split 2-cell, and assertion (i) turns the union of those open cells into the topological frontier.

theorem Schoenflies.CellStructure.SplitData.pos_source_mem_cellUnion_cells₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : R.pos d.source ∈ R.cellUnion d.cells₁

theorem Schoenflies.CellStructure.SplitData.pos_source_mem_cellUnion_cells₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : R.pos d.source ∈ R.cellUnion d.cells₂

theorem Schoenflies.CellStructure.SplitData.pos_target_mem_cellUnion_cells₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : R.pos d.target ∈ R.cellUnion d.cells₁

theorem Schoenflies.CellStructure.SplitData.pos_target_mem_cellUnion_cells₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : R.pos d.target ∈ R.cellUnion d.cells₂

theorem Schoenflies.CellStructure.SplitData.isArcBetween_cellUnion_cells₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : IsArcBetween (R.cellUnion d.cells₁) (R.pos d.source) (R.pos d.target)

A realized boundary path is a simple arc between the ear's two ends.

theorem Schoenflies.CellStructure.SplitData.isArcBetween_cellUnion_cells₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} : IsArcBetween (R.cellUnion d.cells₂) (R.pos d.source) (R.pos d.target)

theorem Schoenflies.CellStructure.SplitData.isCutPair_of_inter {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {D : Set Plane} (hcd : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : IsCutPair (frontier (R.cell d.face)) (R.pos d.source) (R.pos d.target) (R.cellUnion d.cells₁) (R.cellUnion d.cells₂)

The two boundary paths cut the old 2-cell's boundary curve in two.

This is where SplitData.paths_meet is spent, and it is the only place: paths_disjoint alone forbids the two paths a common edge but not a common interior vertex, and with a common interior vertex the two realized paths meet in more than the two cut points. See the module docstring.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.isPathGraph_earGraph {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (d.earGraph earPos).IsPathGraph (R.pos d.source) d.earWalk (R.pos d.target)

The drawn ear is a path graph in the plane.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.isArcBetween_earSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : IsArcBetween (d.earSet earPos earDraw) (R.pos d.source) (R.pos d.target)

The drawn ear is a simple arc between the two old 0-cells it is glued to.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.isCrosscut_earSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {D : Set Plane} (hcd : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : IsCrosscut (frontier (R.cell d.face)) (d.earSet earPos earDraw) (R.pos d.source) (R.pos d.target)

The drawn ear is a crosscut of the old Jordan face.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.closure_edgeArc_diff {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {f a b : γ} (hl : d.ear.IsLink f a b) : closure (Graph.edgeArc earDraw f \ {earPos a, earPos b}) = Graph.edgeArc earDraw f

The closure of an ear edge's open arc is the closed arc.

The realization

noncomputable def Schoenflies.CellStructure.SplitData.realize {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (d : S.SplitData) (earPos : γ → Plane) (earDraw : γ → ℝ → Plane) (hE : d.EarCrosscut R earPos earDraw) : (S.splitFace d).Realization

The realization of a 2-cell split.

The old realization R, a drawing of the ear as a polygonal crosscut of the old open 2-cell, and assertion (i) at the old stage produce a realization of S.splitFace d:

• the ear's interior 0-cells go where the ear's drawing puts them, and its 1-cells to their open arcs;
• the two new 2-cells go to the two sides of the crosscut, inside (Bᵢ ∪ P);
• every surviving cell keeps its old point set.

This is the object the whole split step of lem:cellulation-invariants was missing: SplitData.isCrosscutSplit_realize puts it in the relation IsCrosscutSplit to R, and IsCrosscutSplit.isCellDecomposition_and_isFaceJordan then propagates both invariants.

Equations

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

@[simp]

theorem Schoenflies.CellStructure.SplitData.realize_pos {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (realize R d earPos earDraw hE).pos = d.splitPos R earPos

@[simp]

theorem Schoenflies.CellStructure.SplitData.realize_drawing {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (realize R d earPos earDraw hE).drawing = d.splitDrawing R earDraw

@[simp]

theorem Schoenflies.CellStructure.SplitData.realize_cell {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (realize R d earPos earDraw hE).cell = d.splitCell R earPos earDraw

theorem Schoenflies.CellStructure.SplitData.cellUnion_earCells {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (realize R d earPos earDraw hE).cellUnion d.earCells = d.earSet earPos earDraw

The realized ear is the drawn ear. The open cells of the ear together with the two old 0-cells at its ends occupy exactly the crosscut.

theorem Schoenflies.CellStructure.SplitData.cellUnion_earNewCells {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) : (realize R d earPos earDraw hE).cellUnion d.earNewCells = d.earSet earPos earDraw \ {R.pos d.source, R.pos d.target}

The open cells the ear creates are the crosscut minus its two endpoints.

theorem Schoenflies.CellStructure.SplitData.isCrosscutSplit_realize {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) {D : Set Plane} (hcd : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : d.IsCrosscutSplit R (realize R d earPos earDraw hE)

The constructed realization is a crosscut split of the old one — every clause of SplitData.IsCrosscutSplit, discharged.

Composed with IsCrosscutSplit.isCellDecomposition_and_isFaceJordan this is the whole induction step of lem:cellulation-invariants over the second elementary operation.

theorem Schoenflies.CellStructure.SplitData.isCellDecomposition_and_isFaceJordan_realize {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) (hS : S.CombInvariants) {D : Set Plane} (hcd : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : (realize R d earPos earDraw hE).IsCellDecomposition D ∧ (realize R d earPos earDraw hE).IsFaceJordan ∧ (realize R d earPos earDraw hE).Refines R d.parent

The induction step of lem:cellulation-invariants over the second elementary operation, end to end. From a realization of S satisfying assertions (i) and (vii) and a drawing of the ear as a polygonal crosscut, a realization of S.splitFace d satisfying (i) and (vii), refining it along SplitData.parent.