Generated matched cell structures

The spine of Part II. def:generated-structure says that every cell structure the Schönflies construction ever meets is obtained from the initial two-face structure of prop:initial-pair by a finite sequence of two elementary operations — edge subdivision and 2-cell splitting by an ear — performed simultaneously in the two realizations. This module builds the two operations as defs on Schoenflies.CellStructure, closes them into the inductive Schoenflies.GeneratedStructure, and proves the assertions of lem:cellulation-invariants that are within reach.

Blueprint

• Schoenflies.CellStructure.SubdivData, Schoenflies.CellStructure.subdivideEdge — the first elementary operation of def:generated-structure (tex, operation 1).
• Schoenflies.CellStructure.SplitData, Schoenflies.CellStructure.splitFace — the second (tex, operation 2).
• Schoenflies.GeneratedStructure — def:generated-structure, as the inductive closure of a base structure under the two operations.
• Schoenflies.CellStructure.SubdivData.parent, Schoenflies.CellStructure.SplitData.parent, Schoenflies.CellStructure.SubdivData.sub_parent, Schoenflies.CellStructure.SplitData.sub_parent — assertion (iv) of lem:cellulation-invariants, the parent map of one elementary refinement and the compatibility σ ≼ τ → par σ ≼ par τ.
• Schoenflies.CellStructure.CombInvariants, its two preservation theorems Schoenflies.CellStructure.SubdivData.combInvariants and Schoenflies.CellStructure.SplitData.combInvariants, and Schoenflies.GeneratedStructure.combInvariants, which closes the induction — assertions (iii), (v), (vi), together with the abstract form of (viii) and the bookkeeping facts about ≼_abs that the blueprint uses silently.
• Schoenflies.GeneratedStructure.trans — refinement sequences compose.
• Schoenflies.CellStructure.Realization.IsCellDecomposition — assertion (i) for one realization, and from it, with no further geometry: .frontier_property (assertion (ii)), .sub_iff_subset_closure and Schoenflies.CellStructure.subset_closure_congr (assertion (ix)), and .face_eq (assertion (viii)).
• Schoenflies.CellStructure.SubdivData.IsRefinement and Schoenflies.CellStructure.SubdivData.IsRefinement.isCellDecomposition — the induction step of assertion (i) over the first constructor: a realization of the subdivided structure that refines a realization of the old one inherits (i).
• Schoenflies.crosscut_cell_partition — the geometric content of one 2-cell split, from Schoenflies.general_crosscut, in the shape assertion (i) consumes.

Not here. The induction step of (i) over the second constructor, and assertion (vii) in either. crosscut_cell_partition is the geometric input the split step needs; what is missing is the SplitData analogue of IsRefinement — a relation between a realization of S.splitFace d and one of S, saying that the ear is drawn as a crosscut of the realized open 2-cell — and the identification of the abstract boundary walk of a 2-cell with the Jordan curve of assertion (vii). Assertions (ii), (viii) and (ix) are stated here against (i) as a hypothesis, so later constructors can use the resulting theorem directly.

Two general graph facts are proved here for want of a home: Schoenflies.subdivGraph (with Schoenflies.subdivGraph_mono and Schoenflies.subdivGraph_eq_self) and Schoenflies.isLink_of_le_of_mem_edgeSet. The second belongs in Schoenflies/Graph/; nothing on main states it.

Design

The base case is a parameter. prop:initial-pair is being built elsewhere, so GeneratedStructure S₀ S is relative to an arbitrary base S₀, and every invariant theorem reads "the invariants of S₀ propagate to S". That is both cleaner and independent of the initial pair's schedule: the consumer supplies S₀ and the base case, and gets the invariant at every stage.

rem:intermediate-disconnection is honoured by omission. Nothing in this module mentions Realization.nonboundary, let alone its connectedness: an intermediate stage really can have disconnected open nonboundary part, and every statement here is proved without that hypothesis.

≼_abs stays a raw datum. CellStructure.sub is not made a preorder. The reflexivity and transitivity facts that the blueprint uses are fields of CombInvariants, established for the base and propagated, never assumed of an arbitrary CellStructure.

Fidelity note on reflexivity. The blueprint's two update lists (tex, operations 1 and 2) do not mention the reflexive pairs of the new cells, while the base relation is declared to contain "the reflexive pairs". Assertion (i) forces them: the closure of a new open cell contains that cell, and (i) says a closed cell is the union of its open subcells. Both subRel definitions below therefore declare σ ≼ σ for every new cell; that is the only place where this module adds a pair the blueprint's prose does not list.

Subdividing an edge of a graph

The graph-theoretic half of the first elementary operation, stated for an arbitrary graph so that one definition serves both the skeleton and the outer cycle: when H does not carry e from x to y — which is the case for the outer cycle whenever the subdivided edge is not an outer edge — the construction leaves H alone (subdivGraph_eq_self). Without that, the definition of CellStructure.subdivideEdge would need a case split on whether the subdivided edge is outer, and every lemma about it would inherit the split.

def Schoenflies.subdivGraph {γ : Type u_1} (H : Graph γ γ) (e x y v e₁ e₂ : γ) (hne : e₁ ≠ e₂) (h₁ : e₁ ∉ H.edgeSet) (h₂ : e₂ ∉ H.edgeSet) : Graph γ γ

The graph H with the edge e, running from x to y, replaced by a new vertex v and two new edges e₁ : x — v, e₂ : v — y.

The three guards f ≠ e, f ≠ e₁, f ≠ e₂ on the surviving links make the three disjuncts mutually exclusive with no hypotheses, and hne does the same for the last two. The freshness hypotheses h₁, h₂ are what make edgeSet right.

Equations

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

@[simp]

theorem Schoenflies.subdivGraph_vertexSet {γ : Type u_1} {H : Graph γ γ} {e x y v e₁ e₂ : γ} {hne : e₁ ≠ e₂} {h₁ : e₁ ∉ H.edgeSet} {h₂ : e₂ ∉ H.edgeSet} : (subdivGraph H e x y v e₁ e₂ hne h₁ h₂).vertexSet = H.vertexSet ∪ {z : γ | z = v ∧ H.IsLink e x y}

@[simp]

theorem Schoenflies.subdivGraph_edgeSet {γ : Type u_1} {H : Graph γ γ} {e x y v e₁ e₂ : γ} {hne : e₁ ≠ e₂} {h₁ : e₁ ∉ H.edgeSet} {h₂ : e₂ ∉ H.edgeSet} : (subdivGraph H e x y v e₁ e₂ hne h₁ h₂).edgeSet = H.edgeSet \ {e} ∪ {f : γ | (f = e₁ ∨ f = e₂) ∧ H.IsLink e x y}

theorem Schoenflies.subdivGraph_isLink {γ : Type u_1} {H : Graph γ γ} {e x y v e₁ e₂ : γ} {hne : e₁ ≠ e₂} {h₁ : e₁ ∉ H.edgeSet} {h₂ : e₂ ∉ H.edgeSet} {f a b : γ} : (subdivGraph H e x y v e₁ e₂ hne h₁ h₂).IsLink f a b ↔ H.IsLink f a b ∧ f ≠ e ∧ f ≠ e₁ ∧ f ≠ e₂ ∨ f = e₁ ∧ H.IsLink e x y ∧ s(a, b) = s(x, v) ∨ f = e₂ ∧ H.IsLink e x y ∧ s(a, b) = s(v, y)

theorem Schoenflies.subdivGraph_mono {γ : Type u_1} {H K : Graph γ γ} {e x y v e₁ e₂ : γ} (hHK : H ≤ K) {hne : e₁ ≠ e₂} {h₁ : e₁ ∉ H.edgeSet} {h₂ : e₂ ∉ H.edgeSet} {h₁' : e₁ ∉ K.edgeSet} {h₂' : e₂ ∉ K.edgeSet} : subdivGraph H e x y v e₁ e₂ hne h₁ h₂ ≤ subdivGraph K e x y v e₁ e₂ hne h₁' h₂'

Subdividing is monotone in the graph: a subgraph carrying the subdivided edge is subdivided along with the whole, and one that does not carry it is left alone and still fits inside. This is what gives CellStructure.subdivideEdge its outerGraph_le.

theorem Schoenflies.subdivGraph_eq_self {γ : Type u_1} {H : Graph γ γ} {e x y v e₁ e₂ : γ} {hne : e₁ ≠ e₂} {h₁ : e₁ ∉ H.edgeSet} {h₂ : e₂ ∉ H.edgeSet} (he : e ∉ H.edgeSet) : subdivGraph H e x y v e₁ e₂ hne h₁ h₂ = H

A graph that does not carry the subdivided edge is untouched.

theorem Schoenflies.isLink_of_le_of_mem_edgeSet {γ : Type u_1} {H K : Graph γ γ} {e x y : γ} (hHK : H ≤ K) (he : e ∈ H.edgeSet) (h : K.IsLink e x y) : H.IsLink e x y

An edge of a subgraph has the same ends there as in the ambient graph. General; it is here because nothing on main states it, and both elementary operations need it to know that the outer cycle carries the subdivided edge with its own endpoints.

The cells of an abstract structure

theorem Schoenflies.CellStructure.mem_cells_of_mem_vertexSet {γ : Type u_1} (S : CellStructure γ) {z : γ} (h : z ∈ S.skel.vertexSet) : z ∈ S.cells

theorem Schoenflies.CellStructure.mem_cells_of_mem_edgeSet {γ : Type u_1} (S : CellStructure γ) {z : γ} (h : z ∈ S.skel.edgeSet) : z ∈ S.cells

theorem Schoenflies.CellStructure.mem_cells_of_mem_faces {γ : Type u_1} (S : CellStructure γ) {z : γ} (h : z ∈ S.faces) : z ∈ S.cells

theorem Schoenflies.CellStructure.vertexSet_ne_edgeSet {γ : Type u_1} (S : CellStructure γ) {z w : γ} (hz : z ∈ S.skel.vertexSet) (hw : w ∈ S.skel.edgeSet) : z ≠ w

theorem Schoenflies.CellStructure.faces_ne_vertexSet {γ : Type u_1} (S : CellStructure γ) {z w : γ} (hz : z ∈ S.faces) (hw : w ∈ S.skel.vertexSet) : z ≠ w

theorem Schoenflies.CellStructure.faces_ne_edgeSet {γ : Type u_1} (S : CellStructure γ) {z w : γ} (hz : z ∈ S.faces) (hw : w ∈ S.skel.edgeSet) : z ≠ w

def Schoenflies.CellStructure.pathCells {γ : Type u_1} (S : CellStructure γ) (u : γ) (W : List γ) : Set γ

The cells of a walk: its edges, and the vertices it visits. This is what the blueprint calls "the cells of the boundary walk Bᵢ".

Equations

• S.pathCells u W = {c : γ | c ∈ W} ∪ S.skel.walkVertices u W

theorem Schoenflies.CellStructure.pathCells_subset_cells {γ : Type u_1} {v : γ} {S : CellStructure γ} {u : γ} {W : List γ} (h : S.skel.IsWalk u W v) : S.pathCells u W ⊆ S.cells

Elementary operation 1: edge subdivision

Blueprint, def:generated-structure, operation 1: "the edge e is replaced by a new vertex v and two new edges e₁, e₂, whose endpoints are v together with one old endpoint of e each; the relation ≼_abs is extended by declaring v ≼ e₁ and v ≼ e₂, each old endpoint of e a subcell of its adjacent new edge, and v, e₁, e₂ subcells of exactly the old strict supercells of e; all pairs not involving e are unchanged."

inductive Schoenflies.CellStructure.SubstWalk {γ : Type u_1} (S : CellStructure γ) (edge left right newEdge₁ newEdge₂ : γ) : γ → List γ → List γ → Prop

The orientation-aware replacement of a subdivided edge in a walk. SubstWalk S edge left right newEdge₁ newEdge₂ u W W' says that W' is obtained from W by replacing each traversal of edge by the two new edges in the order in which the walk crosses them. The departing vertex u supplies the orientation information that the edge list alone does not contain.

• nil {γ : Type u_1} {S : CellStructure γ} {edge left right newEdge₁ newEdge₂ : γ} (u : γ) : S.SubstWalk edge left right newEdge₁ newEdge₂ u [] []

  The empty walk is unchanged.

• forward {γ : Type u_1} {S : CellStructure γ} {edge left right newEdge₁ newEdge₂ : γ} {W W' : List γ} (h : S.SubstWalk edge left right newEdge₁ newEdge₂ right W W') : S.SubstWalk edge left right newEdge₁ newEdge₂ left (edge :: W) (newEdge₁ :: newEdge₂ :: W')

  Crossing the subdivided edge from left to right.

• backward {γ : Type u_1} {S : CellStructure γ} {edge left right newEdge₁ newEdge₂ : γ} {W W' : List γ} (h : S.SubstWalk edge left right newEdge₁ newEdge₂ left W W') : S.SubstWalk edge left right newEdge₁ newEdge₂ right (edge :: W) (newEdge₂ :: newEdge₁ :: W')

  Crossing the subdivided edge from right to left.

• other {γ : Type u_1} {S : CellStructure γ} {edge left right newEdge₁ newEdge₂ u w f : γ} {W W' : List γ} (hl : S.skel.IsLink f u w) (hf : f ≠ edge) (h : S.SubstWalk edge left right newEdge₁ newEdge₂ w W W') : S.SubstWalk edge left right newEdge₁ newEdge₂ u (f :: W) (f :: W')

  Any other edge is kept.

structure Schoenflies.CellStructure.SubdivData {γ : Type u_1} (S : CellStructure γ) : Type u_1

The data of one edge subdivision: the edge to be subdivided together with its two endpoints, and three names — fresh, i.e. not cells of S — for the new vertex and the two new edges. It also carries the orientation-aware replacement of every 2-cell boundary walk: the direction in which a walk traverses an edge cannot be recovered from the edge list alone.

The operation is a def of this data, not an existential: everything downstream refers to d.newVertex, d.newEdge₁, d.newEdge₂ and d.newBoundary by name.

• edge : γ

  The subdivided 1-cell.

• left : γ

  One endpoint of the subdivided edge.

• right : γ

  The other endpoint.

• newVertex : γ

  The inserted 0-cell.

• newEdge₁ : γ

  The new 1-cell from left to newVertex.

• newEdge₂ : γ

  The new 1-cell from newVertex to right.

• isLink : S.skel.IsLink self.edge self.left self.right

  edge really runs from left to right.

• newVertex_notMem : self.newVertex ∉ S.cells

  The new vertex is a fresh name.

• newEdge₁_notMem : self.newEdge₁ ∉ S.cells

  The first new edge is a fresh name.

• newEdge₂_notMem : self.newEdge₂ ∉ S.cells

  The second new edge is a fresh name.

• newVertex_ne₁ : self.newVertex ≠ self.newEdge₁

  The three new names are distinct.

• newVertex_ne₂ : self.newVertex ≠ self.newEdge₂

  The three new names are distinct.

• newEdge_ne : self.newEdge₁ ≠ self.newEdge₂

  The three new names are distinct.

• newBoundary : γ → List γ

  The boundary lists after subdivision, chosen with the orientation of each old walk.

• boundary_subst ⦃F : γ⦄ : F ∈ S.faces → ∃ (u : γ), S.skel.IsWalk u (S.boundary F) u ∧ S.SubstWalk self.edge self.left self.right self.newEdge₁ self.newEdge₂ u (S.boundary F) (self.newBoundary F)

  Every face boundary is a closed walk, and its new boundary is obtained by the orientation-aware edge replacement from the same starting vertex.

@[reducible, inline]

abbrev Schoenflies.CellStructure.SubdivData.SubstWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : γ → List γ → List γ → Prop

The orientation-aware replacement relation specialized to the subdivision data.

Equations

• d.SubstWalk = S.SubstWalk d.edge d.left d.right d.newEdge₁ d.newEdge₂

def Schoenflies.CellStructure.SubdivData.newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : Set γ

The three cells the subdivision creates.

Equations

• d.newCells = {d.newVertex, d.newEdge₁, d.newEdge₂}

theorem Schoenflies.CellStructure.SubdivData.notMem_cells_of_mem_newCells {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {z : γ} (h : z ∈ d.newCells) : z ∉ S.cells

theorem Schoenflies.CellStructure.SubdivData.notMem_newCells_of_mem_cells {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {z : γ} (h : z ∈ S.cells) : z ∉ d.newCells

theorem Schoenflies.CellStructure.SubdivData.edge_mem_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.edge ∈ S.skel.edgeSet

theorem Schoenflies.CellStructure.SubdivData.edge_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.edge ∈ S.cells

theorem Schoenflies.CellStructure.SubdivData.left_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.left ∈ S.cells

theorem Schoenflies.CellStructure.SubdivData.right_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.right ∈ S.cells

theorem Schoenflies.CellStructure.SubdivData.newEdge₁_notMem_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.newEdge₁ ∉ S.skel.edgeSet

theorem Schoenflies.CellStructure.SubdivData.newEdge₂_notMem_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.newEdge₂ ∉ S.skel.edgeSet

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

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

def Schoenflies.CellStructure.SubdivData.skeleton {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : Graph γ γ

The subdivided skeleton.

Equations

• d.skeleton = Schoenflies.subdivGraph S.skel d.edge d.left d.right d.newVertex d.newEdge₁ d.newEdge₂ ⋯ ⋯ ⋯

def Schoenflies.CellStructure.SubdivData.outer {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : Graph γ γ

The subdivided outer cycle. When the subdivided edge is not an outer edge this is the old outer cycle unchanged (SubdivData.outer_eq).

Equations

• d.outer = Schoenflies.subdivGraph S.outerGraph d.edge d.left d.right d.newVertex d.newEdge₁ d.newEdge₂ ⋯ ⋯ ⋯

theorem Schoenflies.CellStructure.SubdivData.outer_le_skeleton {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.outer ≤ d.skeleton

@[simp]

theorem Schoenflies.CellStructure.SubdivData.skeleton_vertexSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.skeleton.vertexSet = insert d.newVertex S.skel.vertexSet

@[simp]

theorem Schoenflies.CellStructure.SubdivData.skeleton_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.skeleton.edgeSet = insert d.newEdge₁ (insert d.newEdge₂ (S.skel.edgeSet \ {d.edge}))

theorem Schoenflies.CellStructure.SubdivData.skeleton_isLink {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {f a b : γ} : d.skeleton.IsLink f a b ↔ S.skel.IsLink f a b ∧ f ≠ d.edge ∧ f ≠ d.newEdge₁ ∧ f ≠ d.newEdge₂ ∨ f = d.newEdge₁ ∧ s(a, b) = s(d.left, d.newVertex) ∨ f = d.newEdge₂ ∧ s(a, b) = s(d.newVertex, d.right)

theorem Schoenflies.CellStructure.SubdivData.outer_eq {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (he : d.edge ∉ S.outerGraph.edgeSet) : d.outer = S.outerGraph

The outer cycle is untouched when the subdivided edge is not outer.

theorem Schoenflies.CellStructure.SubdivData.outer_isLink {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (he : d.edge ∈ S.outerGraph.edgeSet) : S.outerGraph.IsLink d.edge d.left d.right

The subdivided edge, when it is outer, is outer with its own two endpoints.

theorem Schoenflies.CellStructure.SubdivData.outer_edgeSet_of_mem {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (he : d.edge ∈ S.outerGraph.edgeSet) : d.outer.edgeSet = insert d.newEdge₁ (insert d.newEdge₂ (S.outerGraph.edgeSet \ {d.edge}))

def Schoenflies.CellStructure.SubdivData.subRel {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : γ → γ → Prop

The abstract subcell relation after an edge subdivision. Read off the blueprint's update list, in order: the old pairs that involve neither e nor a new cell; the reflexive pairs of the new cells (see the fidelity note in the module docstring); v ≼ e₁, e₂; each old endpoint below its adjacent new edge; and the new cells below exactly the old strict supercells of e.

Equations

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

noncomputable def Schoenflies.CellStructure.subdivideEdge {γ : Type u_1} (S : CellStructure γ) (d : S.SubdivData) : CellStructure γ

Elementary operation 1: edge subdivision. The abstract-data update of def:generated-structure, operation 1.

The boundary walks are the orientation-aware replacements carried by SubdivData. They must arrive as data because an edge list does not determine the direction in which its walk crosses the subdivided edge; the two incident face boundaries can traverse it in opposite directions.

Equations

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

@[simp]

theorem Schoenflies.CellStructure.subdivideEdge_skel {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : (S.subdivideEdge d).skel = d.skeleton

@[simp]

theorem Schoenflies.CellStructure.subdivideEdge_faces {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : (S.subdivideEdge d).faces = S.faces

@[simp]

theorem Schoenflies.CellStructure.subdivideEdge_outerGraph {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : (S.subdivideEdge d).outerGraph = d.outer

@[simp]

theorem Schoenflies.CellStructure.subdivideEdge_sub {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ τ : γ} : (S.subdivideEdge d).sub σ τ ↔ d.subRel σ τ

theorem Schoenflies.CellStructure.subdivideEdge_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : (S.subdivideEdge d).cells = S.cells \ {d.edge} ∪ d.newCells

The cells after a subdivision: the old ones except the subdivided edge, plus the three new ones.

Elementary operation 2: splitting a 2-cell by an ear

Blueprint, def:generated-structure, operation 2: "the 2-cell R is replaced by R₁, R₂; the new interior vertices and edges of the ear P are added with their incidences along P (each interior vertex a subcell of its two adjacent ear edges, each ear endpoint a subcell of its adjacent ear edge); the relation ≼_abs is extended by declaring every cell of the boundary walk of Rᵢ, together with every cell of P, a subcell of Rᵢ, for i = 1, 2; no 2-cell is declared a subcell of another, and all pairs not involving R or the new cells are unchanged."

The ear enters as a graph ear together with Graph.IsPathGraph, rather than as a bare list of names: the incidences "along P" are then ear.Inc, and the union S.skel.union ear is the new skeleton with no further bookkeeping.

structure Schoenflies.CellStructure.SplitData {γ : Type u_1} (S : CellStructure γ) : Type u_1

The data of one 2-cell split by an ear: the split 2-cell, two fresh names for the two new 2-cells, and the ear — a path graph whose two ends are old vertices and all of whose other cells are fresh — together with the two boundary paths of the split cell between the ends of the ear.

sub_face is the statement that the two boundary paths carry exactly the cells of the split 2-cell; paths_meet that they meet exactly at the two ends of the ear. Both are consequences of the invariants at the stage being refined, and both are what the blueprint means by "the two boundary paths between its endpoints".

paths_meet used to read paths_disjoint — that the two paths share no edge — and that is too weak. Two edge-disjoint paths between the same two vertices may still share an interior vertex: take parallel edges e₁, f₁ : u — a and e₂, f₂ : a — v and the paths [e₁, e₂], [f₁, f₂]. Every other field holds, and the two realized boundary paths then meet in three points, so IsCutPair.inter_eq — which asks that the two arcs meet exactly at the two cut points — is false, and with it the isCutPair field of SplitData.IsCrosscutSplit, hence assertion (i) at the split constructor. The stronger clause is what a producer actually has, since it picks the two paths as the two arcs of one boundary cycle; paths_disjoint below is recovered from it. Found by the first module that ever built a realization of a split (Schoenflies/RealizeSplit.lean), which had to carry it as a hypothesis.

• face : γ

  The 2-cell being split.

• face₁ : γ

  The first new 2-cell, bounded by path₁ and the ear.

• face₂ : γ

  The second new 2-cell, bounded by path₂ and the ear.

• ear : Graph γ γ

  The inserted ear, as an abstract path graph.

• source : γ

  One end of the ear.

• target : γ

  The other end of the ear.

• earWalk : List γ

  The ear's own edges, in order.

• path₁ : List γ

  The first boundary path of the split 2-cell, from source to target.

• path₂ : List γ

  The second boundary path.

• isPathGraph : self.ear.IsPathGraph self.source self.earWalk self.target

  The ear is a path graph between its two ends.

• isPath₁ : S.skel.IsPath self.source self.path₁ self.target

  The first boundary path really is a path of the skeleton between the ear's ends.

• isPath₂ : S.skel.IsPath self.source self.path₂ self.target

  So is the second.

• ear_disjoint : Disjoint self.ear.vertexSet self.ear.edgeSet

  The ear's vertex names and edge names are distinct.

• source_ne_target : self.source ≠ self.target

  The two ends of the ear are distinct.

• face_mem : self.face ∈ S.faces

  The split cell is a 2-cell.

• vertexSet_inter : self.ear.vertexSet ∩ S.skel.vertexSet = {self.source, self.target}

  The ear meets the old skeleton exactly in its two ends.

• edge_fresh ⦃f : γ⦄ : f ∈ self.ear.edgeSet → f ∉ S.cells

  Every edge of the ear is a fresh name.

• vertex_fresh ⦃z : γ⦄ : z ∈ self.ear.vertexSet → z ≠ self.source → z ≠ self.target → z ∉ S.cells

  Every interior vertex of the ear is a fresh name.

• face₁_notMem : self.face₁ ∉ S.cells

  The first new 2-cell has a fresh name.

• face₂_notMem : self.face₂ ∉ S.cells

  The second new 2-cell has a fresh name.

• face₁_notMem_ear : self.face₁ ∉ self.ear.vertexSet ∪ self.ear.edgeSet

  The first new 2-cell is not a cell of the ear either.

• face₂_notMem_ear : self.face₂ ∉ self.ear.vertexSet ∪ self.ear.edgeSet

  Nor is the second.

• face_ne : self.face₁ ≠ self.face₂

  The two new 2-cells are distinct.

• sub_face ⦃σ : γ⦄ : S.sub σ self.face ↔ σ = self.face ∨ σ ∈ S.pathCells self.source self.path₁ ∪ S.pathCells self.source self.path₂

  The cells below the split 2-cell are exactly the cells of its two boundary paths.

• paths_meet : S.pathCells self.source self.path₁ ∩ S.pathCells self.source self.path₂ = {self.source, self.target}

  The two boundary paths meet exactly at the two ends of the ear. Not merely that they share no edge — see the counterexample in the docstring above.

theorem Schoenflies.CellStructure.SplitData.paths_disjoint {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) ⦃f : γ⦄ (h₁ : f ∈ d.path₁) (h₂ : f ∈ d.path₂) : False

The two boundary paths share no edge, recovered from paths_meet: a common edge would lie in the intersection, hence be one of the two ends, which are 0-cells.

def Schoenflies.CellStructure.SplitData.earCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Set γ

All cells of the ear: its vertices, including its two old ends, and its edges.

Equations

• d.earCells = d.ear.vertexSet ∪ d.ear.edgeSet

def Schoenflies.CellStructure.SplitData.newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Set γ

The cells the split creates: the interior cells of the ear, its edges, and the two new 2-cells. The ear's two ends are not new — they are old vertices, and the blueprint is explicit that they are their own parents.

Equations

• d.newCells = d.ear.vertexSet \ {d.source, d.target} ∪ d.ear.edgeSet ∪ {d.face₁, d.face₂}

def Schoenflies.CellStructure.SplitData.cells₁ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Set γ

The cells of the first boundary path.

Equations

• d.cells₁ = S.pathCells d.source d.path₁

def Schoenflies.CellStructure.SplitData.cells₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Set γ

The cells of the second boundary path.

Equations

• d.cells₂ = S.pathCells d.source d.path₂

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

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

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

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

theorem Schoenflies.CellStructure.SplitData.face_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.face ∈ S.cells

theorem Schoenflies.CellStructure.SplitData.cells₁_subset {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.cells₁ ⊆ S.cells

theorem Schoenflies.CellStructure.SplitData.cells₂_subset {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.cells₂ ⊆ S.cells

theorem Schoenflies.CellStructure.SplitData.mem_cells_of_mem_ear_vertexSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z : γ} (hz : z ∈ d.ear.vertexSet) (h : z ∈ S.cells) : z = d.source ∨ z = d.target

A vertex of the ear other than its two ends is a fresh name; an end is an old vertex.

theorem Schoenflies.CellStructure.SplitData.notMem_cells_of_mem_newCells {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {z : γ} (h : z ∈ d.newCells) : z ∉ S.cells

theorem Schoenflies.CellStructure.SplitData.notMem_newCells_of_mem_cells {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {z : γ} (h : z ∈ S.cells) : z ∉ d.newCells

theorem Schoenflies.CellStructure.SplitData.face_notMem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.face ∉ d.newCells

theorem Schoenflies.CellStructure.SplitData.face₁_mem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.face₁ ∈ d.newCells

theorem Schoenflies.CellStructure.SplitData.face₂_mem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.face₂ ∈ d.newCells

theorem Schoenflies.CellStructure.SplitData.disjoint_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Disjoint S.skel.edgeSet d.ear.edgeSet

theorem Schoenflies.CellStructure.SplitData.compatible {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : S.skel.Compatible d.ear

def Schoenflies.CellStructure.SplitData.skeleton {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Graph γ γ

The skeleton after the split: the old skeleton with the ear glued in along its two ends.

Equations

• d.skeleton = S.skel.union d.ear

@[simp]

theorem Schoenflies.CellStructure.SplitData.skeleton_vertexSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.skeleton.vertexSet = S.skel.vertexSet ∪ d.ear.vertexSet

@[simp]

theorem Schoenflies.CellStructure.SplitData.skeleton_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.skeleton.edgeSet = S.skel.edgeSet ∪ d.ear.edgeSet

theorem Schoenflies.CellStructure.SplitData.le_skeleton {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : S.skel ≤ d.skeleton

theorem Schoenflies.CellStructure.SplitData.ear_le_skeleton {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.ear ≤ d.skeleton

theorem Schoenflies.CellStructure.SplitData.finite_ear_vertexSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.ear.vertexSet.Finite

theorem Schoenflies.CellStructure.SplitData.finite_ear_edgeSet {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.ear.edgeSet.Finite

def Schoenflies.CellStructure.SplitData.subRel {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : γ → γ → Prop

The abstract subcell relation after a 2-cell split. Read off the blueprint's update list, in order: the old pairs involving neither R nor a new cell; the reflexive pairs of the new cells (see the fidelity note in the module docstring); the incidences along the ear; and the cells of P and of Bᵢ, together with Rᵢ itself, below Rᵢ. No 2-cell is below another.

Equations

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

noncomputable def Schoenflies.CellStructure.splitFace {γ : Type u_1} (S : CellStructure γ) (d : S.SplitData) : CellStructure γ

Elementary operation 2: 2-cell splitting by an ear. The abstract-data update of def:generated-structure, operation 2.

As with CellStructure.subdivideEdge, the boundary walks are a raw datum: the two new 2-cells get the concatenation of their boundary path with the reversed ear, and nothing below reads the orientation.

Equations

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

@[simp]

theorem Schoenflies.CellStructure.splitFace_skel {γ : Type u_1} {S : CellStructure γ} (c : S.SplitData) : (S.splitFace c).skel = c.skeleton

@[simp]

theorem Schoenflies.CellStructure.splitFace_faces {γ : Type u_1} {S : CellStructure γ} (c : S.SplitData) : (S.splitFace c).faces = insert c.face₁ (insert c.face₂ (S.faces \ {c.face}))

@[simp]

theorem Schoenflies.CellStructure.splitFace_outerGraph {γ : Type u_1} {S : CellStructure γ} (c : S.SplitData) : (S.splitFace c).outerGraph = S.outerGraph

@[simp]

theorem Schoenflies.CellStructure.splitFace_sub {γ : Type u_1} {S : CellStructure γ} (c : S.SplitData) {σ τ : γ} : (S.splitFace c).sub σ τ ↔ c.subRel σ τ

theorem Schoenflies.CellStructure.splitFace_cells {γ : Type u_1} {S : CellStructure γ} (c : S.SplitData) : (S.splitFace c).cells = S.cells \ {c.face} ∪ c.newCells

The cells after a split: the old ones except the split 2-cell, plus the ear's cells and the two new 2-cells. (The ear's two ends are old cells and appear on both sides.)

Generated matched cell structures

inductive Schoenflies.GeneratedStructure {γ : Type u_1} (S₀ : CellStructure γ) : CellStructure γ → Prop

def:generated-structure: the closure of a base structure under the two elementary operations.

The base is a parameter. The blueprint's base is the initial matched cellulation of prop:initial-pair, which is being built elsewhere; parameterising over it makes every theorem below read "the invariants propagate", with the base case supplied by the producer of S₀.

rem:intermediate-disconnection is honoured by omission: the realizations of a generated structure are required only to be weakly admissible — connectedness of the open nonboundary part is waived — and nothing in this file, or in any statement about GeneratedStructure, mentions that connectedness.

• base {γ : Type u_1} {S₀ : CellStructure γ} : GeneratedStructure S₀ S₀

  The base structure is generated, by the empty sequence of operations.

• subdivideEdge {γ : Type u_1} {S₀ S : CellStructure γ} (h : GeneratedStructure S₀ S) (d : S.SubdivData) : GeneratedStructure S₀ (S.subdivideEdge d)

  Subdividing an edge of a generated structure gives a generated structure.

• splitFace {γ : Type u_1} {S₀ S : CellStructure γ} (h : GeneratedStructure S₀ S) (d : S.SplitData) : GeneratedStructure S₀ (S.splitFace d)

  Splitting a 2-cell of a generated structure by an ear gives a generated structure.

The combinatorial invariants

Assertions (iii), (v) and (vi) of lem:cellulation-invariants, together with the abstract form of (viii) and the bookkeeping facts about ≼_abs that the blueprint's proof uses without comment (the relation relates cells to cells, it is reflexive, and a vertex is below each edge it bounds). They are bundled because the induction propagates them together: the preservation proof of each one reads the others at the previous stage.

structure Schoenflies.CellStructure.CombInvariants {γ : Type u_1} (S : CellStructure γ) : Prop

The combinatorial invariants of lem:cellulation-invariants.

• sub_mem_left ⦃σ τ : γ⦄ : S.sub σ τ → σ ∈ S.cells

  ≼_abs relates cells to cells.

• sub_mem_right ⦃σ τ : γ⦄ : S.sub σ τ → τ ∈ S.cells

  ≼_abs relates cells to cells.

• sub_refl ⦃σ : γ⦄ : σ ∈ S.cells → S.sub σ σ

  ≼_abs is reflexive on cells. The blueprint declares the reflexive pairs in the base relation and preserves them under both constructors.

• sub_isLink ⦃f a b : γ⦄ : S.skel.IsLink f a b → S.sub a f

  Each endpoint of an edge is a subcell of it.

• face_maximal ⦃F τ : γ⦄ : F ∈ S.faces → S.sub F τ → τ = F

  Abstract (viii): no 2-cell is a subcell of anything but itself.

• nonboundary_edge ⦃F : γ⦄ : F ∈ S.faces → ∃ f ∈ S.skel.edgeSet, f ∉ S.outerGraph.edgeSet ∧ S.sub f F

  (iii): every 2-cell boundary contains a nonboundary edge.

• mem_face ⦃σ : γ⦄ : σ ∈ S.cells → ∃ F ∈ S.faces, S.sub σ F

  (v): every cell is a subcell of at least one 2-cell.

• outerEdge_unique : S.OuterEdgeUniqueFace

  (vi): every outer edge is a subcell of exactly one 2-cell.

theorem Schoenflies.CellStructure.CombInvariants.sub_isLink' {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) ⦃f a b : γ⦄ (h : S.skel.IsLink f a b) : S.sub b f

The other endpoint of an edge is below it too.

Edge subdivision preserves the combinatorial invariants

theorem Schoenflies.CellStructure.SubdivData.subRel_of_old {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ τ : γ} (hσc : σ ∈ S.cells) (hτc : τ ∈ S.cells) (hσ : σ ≠ d.edge) (hτ : τ ≠ d.edge) (h : S.sub σ τ) : d.subRel σ τ

theorem Schoenflies.CellStructure.SubdivData.old_subRel_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ τ : γ} (hσc : σ ∈ S.cells) (hτc : τ ∈ S.cells) (hσ : σ ≠ d.edge) (hτ : τ ≠ d.edge) : d.subRel σ τ ↔ S.sub σ τ

On old cells other than the subdivided edge, the relation is unchanged: "all pairs not involving e are unchanged".

theorem Schoenflies.CellStructure.SubdivData.newCells_subRel_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ τ : γ} (hσ : σ ∈ d.newCells) (hτc : τ ∈ S.cells) : d.subRel σ τ ↔ τ ≠ d.edge ∧ S.sub d.edge τ

A new cell is below exactly the old strict supercells of the subdivided edge.

theorem Schoenflies.CellStructure.SubdivData.mem_subdivideEdge_cells_of_old {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {z : γ} (hz : z ∈ S.cells) (hze : z ≠ d.edge) : z ∈ (S.subdivideEdge d).cells

theorem Schoenflies.CellStructure.SubdivData.mem_subdivideEdge_cells_of_new {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {z : γ} (hz : z ∈ d.newCells) : z ∈ (S.subdivideEdge d).cells

theorem Schoenflies.CellStructure.SubdivData.left_ne_edge {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.left ≠ d.edge

theorem Schoenflies.CellStructure.SubdivData.right_ne_edge {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.right ≠ d.edge

theorem Schoenflies.CellStructure.SubdivData.combInvariants {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (hS : S.CombInvariants) : (S.subdivideEdge d).CombInvariants

Edge subdivision preserves the combinatorial invariants: the induction step of assertions (iii), (v), (vi) — and of abstract (viii) — over the first constructor.

The parent map of an edge subdivision

noncomputable def Schoenflies.CellStructure.SubdivData.parent {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : γ → γ

The parent map of one edge subdivision — assertion (iv). The three new cells have the subdivided edge as parent; every surviving cell is its own parent.

Equations

• d.parent σ = if σ ∈ d.newCells then d.edge else σ

theorem Schoenflies.CellStructure.SubdivData.parent_of_mem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ : γ} (h : σ ∈ d.newCells) : d.parent σ = d.edge

theorem Schoenflies.CellStructure.SubdivData.parent_of_notMem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ : γ} (h : σ ∉ d.newCells) : d.parent σ = σ

theorem Schoenflies.CellStructure.SubdivData.parent_of_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {σ : γ} (h : σ ∈ S.cells) : d.parent σ = σ

theorem Schoenflies.CellStructure.SubdivData.sub_parent {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (hS : S.CombInvariants) {σ τ : γ} (h : (S.subdivideEdge d).sub σ τ) : S.sub (d.parent σ) (d.parent τ)

Assertion (iv), the compatibility clause: σ ≼ τ in the refined structure implies par σ ≼ par τ in the old one.

A 2-cell split preserves the combinatorial invariants

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.cells₁_ne_face {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₁) : σ ≠ d.face

theorem Schoenflies.CellStructure.SplitData.cells₂_ne_face {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₂) : σ ≠ d.face

theorem Schoenflies.CellStructure.SplitData.notMem_faces_of_mem_cells₁ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₁) (hσ : σ ∈ S.faces) : False

theorem Schoenflies.CellStructure.SplitData.notMem_faces_of_mem_cells₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₂) (hσ : σ ∈ S.faces) : False

theorem Schoenflies.CellStructure.SplitData.edge_mem_cells₁_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {f : γ} (hf : f ∈ S.skel.edgeSet) : f ∈ d.cells₁ ↔ f ∈ d.path₁

An edge of the skeleton belongs to the cells of a boundary path exactly when it is one of that path's edges — a vertex of the walk cannot be an edge name.

theorem Schoenflies.CellStructure.SplitData.edge_mem_cells₂_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {f : γ} (hf : f ∈ S.skel.edgeSet) : f ∈ d.cells₂ ↔ f ∈ d.path₂

theorem Schoenflies.CellStructure.SplitData.exists_ear_edge {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : ∃ (f : γ), f ∈ d.ear.edgeSet

The ear has at least one edge: its two ends are distinct, so its walk is not empty.

theorem Schoenflies.CellStructure.SplitData.subRel_of_old {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ τ : γ} (hσc : σ ∈ S.cells) (hτc : τ ∈ S.cells) (hσ : σ ≠ d.face) (hτ : τ ≠ d.face) (h : S.sub σ τ) : d.subRel σ τ

theorem Schoenflies.CellStructure.SplitData.old_subRel_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ τ : γ} (hσc : σ ∈ S.cells) (hτc : τ ∈ S.cells) (hσ : σ ≠ d.face) (hτ : τ ≠ d.face) : d.subRel σ τ ↔ S.sub σ τ

On old cells other than the split 2-cell, the relation is unchanged: "all pairs not involving R or the new cells are unchanged".

theorem Schoenflies.CellStructure.SplitData.subRel_face₁_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} : d.subRel σ d.face₁ ↔ σ = d.face₁ ∨ σ ∈ d.earCells ∨ σ ∈ d.cells₁

The cells below the first new 2-cell are exactly the ear's cells, the first boundary path's cells, and itself.

theorem Schoenflies.CellStructure.SplitData.subRel_face₂_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} : d.subRel σ d.face₂ ↔ σ = d.face₂ ∨ σ ∈ d.earCells ∨ σ ∈ d.cells₂

theorem Schoenflies.CellStructure.SplitData.mem_splitFace_cells_of_old {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z : γ} (hz : z ∈ S.cells) (hzf : z ≠ d.face) : z ∈ (S.splitFace d).cells

theorem Schoenflies.CellStructure.SplitData.mem_splitFace_cells_of_new {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z : γ} (hz : z ∈ d.newCells) : z ∈ (S.splitFace d).cells

theorem Schoenflies.CellStructure.SplitData.mem_splitFace_cells_of_ear {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z : γ} (hz : z ∈ d.earCells) : z ∈ (S.splitFace d).cells

theorem Schoenflies.CellStructure.SplitData.combInvariants {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (hS : S.CombInvariants) : (S.splitFace d).CombInvariants

A 2-cell split preserves the combinatorial invariants: the induction step of assertions (iii), (v), (vi) — and of abstract (viii) — over the second constructor.

The parent map of a 2-cell split

noncomputable def Schoenflies.CellStructure.SplitData.parent {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : γ → γ

The parent map of one 2-cell split — assertion (iv). The ear's interior cells and both new 2-cells have the split 2-cell as parent; every surviving cell — including the ear's two endpoints, which the split does not create — is its own parent.

Equations

• d.parent σ = if σ ∈ d.newCells then d.face else σ

theorem Schoenflies.CellStructure.SplitData.parent_of_mem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.newCells) : d.parent σ = d.face

theorem Schoenflies.CellStructure.SplitData.parent_of_notMem_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∉ d.newCells) : d.parent σ = σ

theorem Schoenflies.CellStructure.SplitData.parent_of_mem_cells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ S.cells) : d.parent σ = σ

theorem Schoenflies.CellStructure.SplitData.sub_parent_of_mem_cells₁ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₁) : S.sub (d.parent σ) d.face

theorem Schoenflies.CellStructure.SplitData.sub_parent_of_mem_cells₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {σ : γ} (h : σ ∈ d.cells₂) : S.sub (d.parent σ) d.face

theorem Schoenflies.CellStructure.SplitData.sub_parent_of_mem_earCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (hS : S.CombInvariants) {σ : γ} (h : σ ∈ d.earCells) : S.sub (d.parent σ) d.face

theorem Schoenflies.CellStructure.SplitData.sub_parent {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (hS : S.CombInvariants) {σ τ : γ} (h : (S.splitFace d).sub σ τ) : S.sub (d.parent σ) (d.parent τ)

Assertion (iv), the compatibility clause, for a 2-cell split.

The invariants at every stage

theorem Schoenflies.GeneratedStructure.combInvariants {γ : Type u_1} {S₀ S : CellStructure γ} (h : GeneratedStructure S₀ S) (h₀ : S₀.CombInvariants) : S.CombInvariants

Assertions (iii), (v), (vi) and abstract (viii) hold at every generated stage. The induction is over the two constructors; the base case is supplied by the producer of S₀ — prop:initial-pair for the blueprint's own generated structures.

theorem Schoenflies.GeneratedStructure.trans {γ : Type u_1} {S₀ S₁ S₂ : CellStructure γ} (h₁ : GeneratedStructure S₀ S₁) (h₂ : GeneratedStructure S₁ S₂) : GeneratedStructure S₀ S₂

Refinement sequences compose. A structure generated from S₁, itself generated from S₀, is generated from S₀. thm:finite-transfer builds its stages one ear at a time and needs exactly this.

theorem Schoenflies.CellStructure.sub_parent_comp {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d₁ : S.SubdivData) (d₂ : (S.subdivideEdge d₁).SplitData) {σ τ : γ} (h : ((S.subdivideEdge d₁).splitFace d₂).sub σ τ) : S.sub (d₁.parent (d₂.parent σ)) (d₁.parent (d₂.parent τ))

The composite parent map of a full ear insertion. The blueprint inserts an ear only after subdividing its endpoint cells if necessary, and remarks that the composite parent map then sends such an endpoint to the pre-subdivision edge. Compatibility composes along with it: this is assertion (iv) for the two-step refinement.

The geometric assertions

Assertion (i) is the only geometric input the rest need: (ii), (viii) and (ix) follow from it formally, with no further topology beyond "a nonempty open set contained in a closure meets the set". That is why they are stated here for an arbitrary realization satisfying (i), rather than by induction: the induction is entirely in (i) and (vii), and those are the standing gap of this module.

structure Schoenflies.CellStructure.Realization.IsCellDecomposition {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (D : Set Plane) : Prop

Assertion (i) of lem:cellulation-invariants, for one realization: the open cells are nonempty and pairwise disjoint, they cover the closed domain D, and every closed cell is the union of its open subcells — the last clause read against the abstract relation ≼_abs, which is what makes (ix) a formal consequence.

• nonempty ⦃σ : γ⦄ : σ ∈ S.cells → (R.cell σ).Nonempty

  Every open cell is nonempty.

• disjoint ⦃σ τ : γ⦄ : σ ∈ S.cells → τ ∈ S.cells → σ ≠ τ → Disjoint (R.cell σ) (R.cell τ)

  Distinct open cells are disjoint.

• iUnion_eq : ⋃ σ ∈ S.cells, R.cell σ = D

  The open cells cover the closed domain.

• closure_eq ⦃τ : γ⦄ : τ ∈ S.cells → closure (R.cell τ) = ⋃ σ ∈ {σ : γ | σ ∈ S.cells ∧ S.sub σ τ}, R.cell σ

  Every closed cell is the union of its open subcells.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.subset_closure {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) (hsub : S.sub σ τ) : R.cell σ ⊆ closure (R.cell τ)

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_of_mem {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) {z : Plane} (hzσ : z ∈ R.cell σ) (hzτ : z ∈ closure (R.cell τ)) : S.sub σ τ

A point of an open cell lying in a closed cell forces the abstract relation. This is the one step of the argument; everything below is a corollary of it.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_of_subset_closure {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) (hsub : R.cell σ ⊆ closure (R.cell τ)) : S.sub σ τ

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_iff_subset_closure {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) : S.sub σ τ ↔ R.cell σ ⊆ closure (R.cell τ)

Assertion (ix) for one realization: the abstract subcell relation is geometric containment.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.frontier_property {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) : R.cell σ ⊆ closure (R.cell τ) ∨ Disjoint (R.cell σ) (closure (R.cell τ))

Assertion (ii), the frontier property: an open cell is either inside a closed cell or misses it. It is a formal consequence of (i) — a closed cell is a union of open cells, and two open cells that meet are equal.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_refl {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) : S.sub σ σ

On a structure with a cell decomposition ≼_abs is reflexive on cells — the blueprint's "each geometric relation is reflexive". It is not assumed of a CellStructure; it is read off (i).

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_trans {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {σ τ ρ : γ} (h : R.IsCellDecomposition D) (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) (hρ : ρ ∈ S.cells) (h₁ : S.sub σ τ) (h₂ : S.sub τ ρ) : S.sub σ ρ

…and transitive, for the same reason.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.face_eq {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) {F T : γ} (hF : F ∈ S.faces) (hT : T ∈ S.faces) (hopen : IsOpen (R.cell F)) (hsub : R.cell F ⊆ closure (R.cell T)) : F = T

Assertion (viii): distinct open 2-cells are never comparable.

The hypothesis is that the lower 2-cell is open, which is what assertion (vii) supplies — it realizes each open 2-cell as the bounded complementary region of a Jordan curve. Given that, thm:jordan is not needed a second time: a nonempty open set inside a closure meets the set.

theorem Schoenflies.CellStructure.subset_closure_congr {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ : Set Plane} (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) {σ τ : γ} (hσ : σ ∈ S.cells) (hτ : τ ∈ S.cells) : (R₁.cell σ ⊆ closure (R₁.cell τ) ↔ R₂.cell σ ⊆ closure (R₂.cell τ)) ∧ (S.sub σ τ ↔ R₁.cell σ ⊆ closure (R₁.cell τ)) ∧ (S.sub σ τ ↔ R₂.cell σ ⊆ closure (R₂.cell τ))

Assertion (ix), in full: geometric containment in the source realization, geometric containment in the target realization, and the abstract relation, all coincide. Both realizations realize the same abstract S, so there is nothing to transport — the two geometric relations are equal because each equals ≼_abs.

Assertion (i) is preserved by an edge subdivision

The induction step of (i) over the first constructor. It relates two realizations of two different structures, so it needs a name for "R' refines R along d": that is SubdivData.IsRefinement, whose fields are exactly the blueprint's sentence "the corresponding point is inserted into the corresponding edge using the edge parametrization", read as a statement about the resulting open cells and their closures.

structure Schoenflies.CellStructure.SubdivData.IsRefinement {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (R' : (S.subdivideEdge d).Realization) : Prop

R' refines R along the subdivision d. Every surviving cell stays where it was; the old open edge is cut into the two new open edges and the new vertex; and the closure of each new cell is the new cell together with the cells the update declares below it.

• cell_eq ⦃σ : γ⦄ : σ ∈ S.cells → σ ≠ d.edge → R'.cell σ = R.cell σ

  Surviving cells are unmoved.

• cell_edge : R.cell d.edge = R'.cell d.newEdge₁ ∪ R'.cell d.newVertex ∪ R'.cell d.newEdge₂

  The old open edge is cut in three.

• nonempty ⦃σ : γ⦄ : σ ∈ d.newCells → (R'.cell σ).Nonempty

  The three new open cells are nonempty.

• disjoint ⦃σ τ : γ⦄ : σ ∈ d.newCells → τ ∈ d.newCells → σ ≠ τ → Disjoint (R'.cell σ) (R'.cell τ)

  …and pairwise disjoint.

• closure_newVertex : closure (R'.cell d.newVertex) = R'.cell d.newVertex

  The new vertex is a closed cell.

• closure_newEdge₁ : closure (R'.cell d.newEdge₁) = R'.cell d.newEdge₁ ∪ R'.cell d.newVertex ∪ R.cell d.left

  The closure of the first new edge is it, the new vertex and the old left endpoint.

• closure_newEdge₂ : closure (R'.cell d.newEdge₂) = R'.cell d.newEdge₂ ∪ R'.cell d.newVertex ∪ R.cell d.right

  The closure of the second new edge is it, the new vertex and the old right endpoint.

theorem Schoenflies.CellStructure.SubdivData.subRel_newVertex_iff {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d : S.SubdivData) {σ : γ} : d.subRel σ d.newVertex ↔ σ = d.newVertex

Nothing is below the new vertex but the new vertex.

theorem Schoenflies.CellStructure.SubdivData.subRel_newEdge₁_iff {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d : S.SubdivData) {σ : γ} : d.subRel σ d.newEdge₁ ↔ σ = d.newEdge₁ ∨ σ = d.newVertex ∨ σ = d.left

The cells below the first new edge are it, the new vertex, and the old left endpoint.

theorem Schoenflies.CellStructure.SubdivData.subRel_newEdge₂_iff {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d : S.SubdivData) {σ : γ} : d.subRel σ d.newEdge₂ ↔ σ = d.newEdge₂ ∨ σ = d.newVertex ∨ σ = d.right

The cells below the second new edge are it, the new vertex, and the old right endpoint.

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.cell_subset_edge {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {R' : (S.subdivideEdge d).Realization} (href : d.IsRefinement R R') {σ : γ} (hσ : σ ∈ d.newCells) : R'.cell σ ⊆ R.cell d.edge

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.isCellDecomposition {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {R' : (S.subdivideEdge d).Realization} {D : Set Plane} (hS : S.CombInvariants) (href : d.IsRefinement R R') (h : R.IsCellDecomposition D) : R'.IsCellDecomposition D

Assertion (i) is preserved by an edge subdivision.

The geometric content of one 2-cell split

thm:general-crosscut is what the induction step of assertions (i) and (vii) applies at each split. The two hypotheses it still carries on main — thm:jordan and HasArcCollars — are threaded through verbatim; both are being discharged elsewhere.

theorem Schoenflies.IsCrosscut.inside_inter {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : inside C ∩ P = P \ {p, q}

The crosscut meets the Jordan domain exactly in its own interior points.

theorem Schoenflies.IsCrosscut.inside_eq_split {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : inside C = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∪ P \ {p, q}

The Jordan domain is the disjoint union of the two sides and the open crosscut. This is the shape assertion (i) consumes at a 2-cell split: the old open 2-cell is partitioned into the two new open 2-cells together with the open cells of the ear (here the ear is one open edge, its two endpoints being old cells).

theorem Schoenflies.IsCrosscut.disjoint_side_crosscut {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : Disjoint (inside (A₁ ∪ P)) (P \ {p, q})

Each side misses the crosscut.

theorem Schoenflies.crosscut_cell_partition {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) (hcollars : HasArcCollars (inside C) P) : inside C = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∪ P \ {p, q} ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ Disjoint (inside (A₁ ∪ P)) (P \ {p, q}) ∧ Disjoint (inside (A₂ ∪ P)) (P \ {p, q}) ∧ IsOpen (inside (A₁ ∪ P)) ∧ IsOpen (inside (A₂ ∪ P)) ∧ (inside (A₁ ∪ P)).Nonempty ∧ (inside (A₂ ∪ P)).Nonempty ∧ closure (inside (A₁ ∪ P)) = inside (A₁ ∪ P) ∪ (A₁ ∪ P) ∧ closure (inside (A₂ ∪ P)) = inside (A₂ ∪ P) ∪ (A₂ ∪ P)

One 2-cell split, geometrically — the induction step of assertions (i) and (vii), assembled from Schoenflies.general_crosscut.

The old open 2-cell Int(C) is the disjoint union of the two new open 2-cells and the open crosscut; each new open 2-cell is open and nonempty; and the closure of each is that open 2-cell together with its own boundary curve Aᵢ ∪ P, which is "every closed cell is the union of its open subcells" for the two new 2-cells.