Realizing an edge subdivision

Schoenflies/GeneratedStructure.lean performs the abstract edge subdivision (CellStructure.subdivideEdge) and states what it means for a realization of the subdivided structure to refine a realization of the old one (SubdivData.IsRefinement); Schoenflies/CellulationInvariants.lean propagates assertions (i), (iv) and (vii) across such a refinement. Nothing built such a realization. This module does.

The construction is the blueprint's own sentence — "the corresponding point is inserted into the corresponding edge using the edge parametrization" — made into data: pick a parameter t ∈ (0,1), put the new 0-cell at R.drawing d.edge t, and draw the two new 1-cells with the two halves of the old parametrization, each rescaled to [0,1].

The orientation of the drawn edge

IsDrawing.edge_param is deliberately orientation-free: it says G.IsLink e (drawing e 0) (drawing e 1), so drawing d.edge 0 may be either pos d.left or pos d.right. But d.newEdge₁ runs from d.left to d.newVertex by definition of subdivideEdge, so which half of the parametrization draws it is not fixed in advance.

Assuming drawing d.edge 0 = pos d.left would be a false hypothesis for half of all inputs, and the caller cannot repair it (swapping d.left with d.right in the SubdivData also swaps the two new edge names, producing a different abstract structure). So the orientation is read off instead: SubdivData.leftParam is the endpoint parameter, 0 or 1, at which the drawn edge sits at d.left. Every statement below is orientation-free; only the two lemmas SubdivData.drawing_leftParam and SubdivData.drawing_rightParam look inside.

Because of that, the construction is phrased with Schoenflies.subarc — the general affine reparametrization already on main — rather than with firstHalf / secondHalf, which are the two halves in the standard orientation and are recorded here as the named special case.

No side conditions

SubdivData.realize takes no geometric hypothesis beyond t ∈ Ioo 0 1. Everything else it needs — that d.edge is drawn, injectively and continuously, between the positions of d.left and d.right, and that an interior point of a drawn edge is not a vertex — is already carried by CellStructure.Realization, and is extracted here rather than assumed.

The transported skeleton homeomorphism is not here, but it exists

Closed, in Schoenflies/RealizeSubdivHomeo.lean (SubdivData.realizeHomeo), on top of Schoenflies/ArcMonotone.lean, which supplies the missing fact named at the end of this section. What follows is the record of why it could not be done here.

SkeletonHomeo.realize is absent from this module. Six of its eight fields are immediate — skeletonSet_realize below says the realized 1-skeleton is literally the same set after a subdivision, so the map, its inverse, both continuity clauses and both inverse clauses transport verbatim, and pos_apply at the new 0-cell is the statement g.toFun (R₁.drawing d.edge t₁) = R₂.drawing d.edge t₂ that a caller choosing corresponding parameters supplies anyway.

What is missing is edgeArc_image at the two new edges: that g carries the half arc from R₁.pos d.left to the new source point onto the half arc from R₂.pos d.left to the new target point. This is true but is not implied by the SkeletonHomeo data pointwise: it needs the fact that a homeomorphism between two arcs matching their endpoints is monotone, hence carries initial subarcs to initial subarcs. That fact was not on main when this module was written, and assuming the two clauses would have been assuming the conclusion, so nothing was stated here. Schoenflies/ArcMonotone.lean now proves it — ArcMatch, transferParam, image_image_uIcc — and Schoenflies/RealizeSubdivHomeo.lean builds the transported homeomorphism from it, orientation of the two realizations handled rather than assumed.

Blueprint

• def:generated-structure, operation 1 (edge subdivision) — the geometric half of the operation, whose abstract half is CellStructure.subdivideEdge.
• lem:cellulation-invariants (i) and (iv), the paragraph "Suppose first that an open edge e is subdivided at a new vertex v": SubdivData.isRefinement_realize produces exactly the hypotheses that SubdivData.IsRefinement.isCellDecomposition_and_isFaceJordan consumes.

Declarations:

• Schoenflies.uIcc_union_uIcc, Schoenflies.uIcc_inter_uIcc — a parameter interval cut at an interior point.
• Schoenflies.subarc_image_union, Schoenflies.subarc_image_inter — the two subarcs of a cut cover the arc and meet exactly at the cut point.
• Schoenflies.firstHalf, Schoenflies.secondHalf — the two halves of a drawn edge in the standard orientation, with their endpoint values, continuity, injectivity, images, meet and union.
• Schoenflies.CellStructure.SubdivData.leftParam / rightParam — the orientation of the drawn edge.
• Schoenflies.CellStructure.SubdivData.realize — the realization of the subdivided structure.
• Schoenflies.CellStructure.SubdivData.isRefinement_realize — it refines the given one.
• Schoenflies.CellStructure.SubdivData.realize_isCellDecomposition_and_isFaceJordan — the induction step of lem:cellulation-invariants over the first constructor, now constructed with all necessary data constructed here.
• Schoenflies.CellStructure.SubdivData.skeletonSet_realize — a subdivision does not move the realized 1-skeleton.

Cutting a parameter interval at an interior point

theorem Schoenflies.uIcc_union_uIcc {a b t : ℝ} (h : t ∈ Set.uIcc a b) : Set.uIcc a t ∪ Set.uIcc t b = Set.uIcc a b

The two halves of a parameter interval cut at a point of it cover it.

theorem Schoenflies.uIcc_inter_uIcc {a b t : ℝ} (h : t ∈ Set.uIcc a b) : Set.uIcc a t ∩ Set.uIcc t b = {t}

…and meet exactly at the cut point.

theorem Schoenflies.right_notMem_uIcc_left {a b t : ℝ} (h : t ∈ Set.uIcc a b) (hb : b ≠ t) : b ∉ Set.uIcc a t

The far endpoint is not in the near half.

theorem Schoenflies.left_notMem_uIcc_right {a b t : ℝ} (h : t ∈ Set.uIcc a b) (ha : a ≠ t) : a ∉ Set.uIcc t b

…and symmetrically.

theorem Schoenflies.uIcc_left_subset {a b t : ℝ} (h : t ∈ Set.uIcc a b) : Set.uIcc a t ⊆ Set.uIcc a b

theorem Schoenflies.uIcc_right_subset {a b t : ℝ} (h : t ∈ Set.uIcc a b) : Set.uIcc t b ⊆ Set.uIcc a b

The two subarcs of a cut

theorem Schoenflies.subarc_image_union {a b t : ℝ} {f : ℝ → Plane} (h : t ∈ Set.uIcc a b) : subarc f a t '' unitInterval ∪ subarc f t b '' unitInterval = f '' Set.uIcc a b

The two subarcs of a cut cover the arc.

theorem Schoenflies.subarc_image_inter {a b t : ℝ} {f : ℝ → Plane} (hi : Set.InjOn f (Set.uIcc a b)) (h : t ∈ Set.uIcc a b) : subarc f a t '' unitInterval ∩ subarc f t b '' unitInterval = {f t}

The two subarcs of a cut meet exactly at the cut point.

theorem Schoenflies.IsArcBetween.closure_diff_eq {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : closure (A \ {p, q}) = A

The closure of an open arc is the closed arc.

theorem Schoenflies.diff_pair_union_union {A : Set Plane} {p q : Plane} (hp : p ∈ A) (hq : q ∈ A) : A \ {p, q} ∪ {q} ∪ {p} = A

The three pieces an open arc is cut into put the arc back together.

The two halves of a drawn edge

The special case a = 0, b = 1 of the previous section, in the notation a consumer holding a Graph.IsDrawing writes.

theorem Schoenflies.uIcc_zero_one : Set.uIcc 0 1 = unitInterval

def Schoenflies.firstHalf {β : Type u_1} (drawing : β → ℝ → Plane) (e : β) (t : ℝ) : ℝ → Plane

The first half of a drawn edge, rescaled to [0, 1].

Equations

• Schoenflies.firstHalf drawing e t = Schoenflies.subarc (drawing e) 0 t

def Schoenflies.secondHalf {β : Type u_1} (drawing : β → ℝ → Plane) (e : β) (t : ℝ) : ℝ → Plane

The second half of a drawn edge, rescaled to [0, 1].

Equations

• Schoenflies.secondHalf drawing e t = Schoenflies.subarc (drawing e) t 1

theorem Schoenflies.firstHalf_apply {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (s : ℝ) : firstHalf drawing e t s = drawing e (t * s)

theorem Schoenflies.secondHalf_apply {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (s : ℝ) : secondHalf drawing e t s = drawing e (t + (1 - t) * s)

@[simp]

theorem Schoenflies.firstHalf_zero {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} : firstHalf drawing e t 0 = drawing e 0

@[simp]

theorem Schoenflies.firstHalf_one {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} : firstHalf drawing e t 1 = drawing e t

@[simp]

theorem Schoenflies.secondHalf_zero {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} : secondHalf drawing e t 0 = drawing e t

@[simp]

theorem Schoenflies.secondHalf_one {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} : secondHalf drawing e t 1 = drawing e 1

theorem Schoenflies.continuousOn_firstHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hc : ContinuousOn (drawing e) unitInterval) (ht : t ∈ unitInterval) : ContinuousOn (firstHalf drawing e t) unitInterval

theorem Schoenflies.continuousOn_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hc : ContinuousOn (drawing e) unitInterval) (ht : t ∈ unitInterval) : ContinuousOn (secondHalf drawing e t) unitInterval

theorem Schoenflies.injOn_firstHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hi : Set.InjOn (drawing e) unitInterval) (ht : t ∈ unitInterval) (h0 : t ≠ 0) : Set.InjOn (firstHalf drawing e t) unitInterval

theorem Schoenflies.injOn_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hi : Set.InjOn (drawing e) unitInterval) (ht : t ∈ unitInterval) (h1 : t ≠ 1) : Set.InjOn (secondHalf drawing e t) unitInterval

theorem Schoenflies.image_firstHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (ht : t ∈ unitInterval) : firstHalf drawing e t '' unitInterval = drawing e '' Set.Icc 0 t

theorem Schoenflies.image_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (ht : t ∈ unitInterval) : secondHalf drawing e t '' unitInterval = drawing e '' Set.Icc t 1

theorem Schoenflies.firstHalf_union_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (ht : t ∈ unitInterval) : firstHalf drawing e t '' unitInterval ∪ secondHalf drawing e t '' unitInterval = Graph.edgeArc drawing e

The two halves cover the drawn edge.

theorem Schoenflies.firstHalf_inter_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hi : Set.InjOn (drawing e) unitInterval) (ht : t ∈ unitInterval) : firstHalf drawing e t '' unitInterval ∩ secondHalf drawing e t '' unitInterval = {drawing e t}

The two halves meet exactly at the cut point.

theorem Schoenflies.isArcBetween_firstHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hc : ContinuousOn (drawing e) unitInterval) (hi : Set.InjOn (drawing e) unitInterval) (ht : t ∈ unitInterval) (h0 : t ≠ 0) : IsArcBetween (firstHalf drawing e t '' unitInterval) (drawing e 0) (drawing e t)

Each half is an arc between the corresponding endpoint and the cut point.

theorem Schoenflies.isArcBetween_secondHalf {t : ℝ} {β : Type u_1} {drawing : β → ℝ → Plane} {e : β} (hc : ContinuousOn (drawing e) unitInterval) (hi : Set.InjOn (drawing e) unitInterval) (ht : t ∈ unitInterval) (h1 : t ≠ 1) : IsArcBetween (secondHalf drawing e t '' unitInterval) (drawing e t) (drawing e 1)

The orientation of the drawn subdivided edge

theorem Schoenflies.CellStructure.SubdivData.edge_mem_edgeSet_graph {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : d.edge ∈ R.graph.edgeSet

What the realization already knows about the subdivided edge: it is an edge of the drawn skeleton.

theorem Schoenflies.CellStructure.SubdivData.continuousOn_drawing_edge {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : ContinuousOn (R.drawing d.edge) unitInterval

theorem Schoenflies.CellStructure.SubdivData.injOn_drawing_edge {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : Set.InjOn (R.drawing d.edge) unitInterval

theorem Schoenflies.CellStructure.SubdivData.isLink_drawn_edge {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : R.graph.IsLink d.edge (R.pos d.left) (R.pos d.right)

noncomputable def Schoenflies.CellStructure.SubdivData.leftParam {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : ℝ

The orientation of the drawn subdivided edge: the endpoint parameter, 0 or 1, at which R.drawing d.edge sits at R.pos d.left.

IsDrawing.edge_param fixes only the unordered pair of endpoint values, so this cannot be read off the structure; it is decided by a case distinction, once, here.

Equations

• d.leftParam R = if R.drawing d.edge 0 = R.pos d.left then 0 else 1

noncomputable def Schoenflies.CellStructure.SubdivData.rightParam {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : ℝ

The endpoint parameter at which the drawn subdivided edge sits at R.pos d.right.

Equations

• d.rightParam R = 1 - d.leftParam R

theorem Schoenflies.CellStructure.SubdivData.leftParam_eq_zero_or_one {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : d.leftParam R = 0 ∨ d.leftParam R = 1

theorem Schoenflies.CellStructure.SubdivData.drawing_params {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : R.drawing d.edge (d.leftParam R) = R.pos d.left ∧ R.drawing d.edge (d.rightParam R) = R.pos d.right

The two endpoint parameters land on the two endpoints. The only lemma that looks inside leftParam; everything downstream is orientation-free.

theorem Schoenflies.CellStructure.SubdivData.drawing_leftParam {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : R.drawing d.edge (d.leftParam R) = R.pos d.left

theorem Schoenflies.CellStructure.SubdivData.drawing_rightParam {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : R.drawing d.edge (d.rightParam R) = R.pos d.right

theorem Schoenflies.CellStructure.SubdivData.leftParam_mem_I {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : d.leftParam R ∈ unitInterval

theorem Schoenflies.CellStructure.SubdivData.rightParam_mem_I {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : d.rightParam R ∈ unitInterval

theorem Schoenflies.CellStructure.SubdivData.uIcc_params {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) : Set.uIcc (d.leftParam R) (d.rightParam R) = unitInterval

The two endpoint parameters span the whole parameter interval, in whichever order.

theorem Schoenflies.CellStructure.SubdivData.leftParam_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (ht : t ∈ Set.Ioo 0 1) : d.leftParam R ≠ t

theorem Schoenflies.CellStructure.SubdivData.rightParam_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (ht : t ∈ Set.Ioo 0 1) : d.rightParam R ≠ t

theorem Schoenflies.CellStructure.SubdivData.mem_uIcc_params {t : ℝ} {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (ht : t ∈ Set.Ioo 0 1) : t ∈ Set.uIcc (d.leftParam R) (d.rightParam R)

theorem Schoenflies.CellStructure.SubdivData.newPos_notMem_vertexSet {t : ℝ} {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (ht : t ∈ Set.Ioo 0 1) : R.drawing d.edge t ∉ R.graph.vertexSet

An interior point of a drawn edge is not a vertex. The one geometric fact the construction needs that is not simply read off a field, and the reason SubdivData.realize needs no side condition.

theorem Schoenflies.CellStructure.SubdivData.newPos_ne_pos {t : ℝ} {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (ht : t ∈ Set.Ioo 0 1) {v : γ} (hv : v ∈ S.skel.vertexSet) : R.drawing d.edge t ≠ R.pos v

Freshness of the three new names, in the forms used below

theorem Schoenflies.CellStructure.SubdivData.newVertex_notMem_vertexSet {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) : d.newVertex ∉ S.skel.vertexSet

theorem Schoenflies.CellStructure.SubdivData.ne_newVertex_of_mem_cells {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) {z : γ} (hz : z ∈ S.cells) : z ≠ d.newVertex

theorem Schoenflies.CellStructure.SubdivData.ne_newEdge₁_of_mem_cells {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) {z : γ} (hz : z ∈ S.cells) : z ≠ d.newEdge₁

theorem Schoenflies.CellStructure.SubdivData.ne_newEdge₂_of_mem_cells {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) {z : γ} (hz : z ∈ S.cells) : z ≠ d.newEdge₂

theorem Schoenflies.CellStructure.SubdivData.newEdge₁_ne_edge {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) : d.newEdge₁ ≠ d.edge

theorem Schoenflies.CellStructure.SubdivData.newEdge₂_ne_edge {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) : d.newEdge₂ ≠ d.edge

The links of the subdivided skeleton

theorem Schoenflies.CellStructure.SubdivData.isLink_newEdge₁ {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) : d.skeleton.IsLink d.newEdge₁ d.left d.newVertex

theorem Schoenflies.CellStructure.SubdivData.isLink_newEdge₂ {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) : d.skeleton.IsLink d.newEdge₂ d.newVertex d.right

theorem Schoenflies.CellStructure.SubdivData.skeleton_isLink_of_old {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) {f x y : γ} (hfe : f ≠ d.edge) (h : S.skel.IsLink f x y) : d.skeleton.IsLink f x y

An old edge other than the subdivided one keeps its ends.

theorem Schoenflies.CellStructure.SubdivData.skeleton_isLink_old_iff {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) {f x y : γ} (hf : f ∈ S.skel.edgeSet) (hfe : f ≠ d.edge) : d.skeleton.IsLink f x y ↔ S.skel.IsLink f x y

…and gains none: for an old edge the two skeleta have the same links.

The realization of the subdivided structure

noncomputable def Schoenflies.CellStructure.SubdivData.realizePos {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (t : ℝ) : γ → Plane

The positions after the subdivision: the new 0-cell goes to the point of the drawn edge at parameter t, and every old 0-cell stays where it was.

Equations

• d.realizePos R t z = if z = d.newVertex then R.drawing d.edge t else R.pos z

noncomputable def Schoenflies.CellStructure.SubdivData.realizeDrawing {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (t : ℝ) : γ → ℝ → Plane

The parametrizations after the subdivision: the two new 1-cells are drawn by the two halves of the old parametrization, cut at t and rescaled to [0, 1]; every old 1-cell keeps its own.

d.newEdge₁ runs from d.left, so the half that draws it starts at d.leftParam R, which is 0 or 1 according to the orientation of the old parametrization.

Equations

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

noncomputable def Schoenflies.CellStructure.SubdivData.realizeCell {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (t : ℝ) : γ → Set Plane

The open cells after the subdivision: the new 0-cell is the new point, each new open 1-cell is its half arc without its two endpoints, and every surviving cell is unchanged.

Equations

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

noncomputable def Schoenflies.CellStructure.SubdivData.realizeGraph {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (t : ℝ) : Graph Plane γ

The drawn skeleton after the subdivision.

Equations

• d.realizeGraph R t = Graph.map (d.realizePos R t) d.skeleton

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizePos_newVertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizePos R t d.newVertex = R.drawing d.edge t

theorem Schoenflies.CellStructure.SubdivData.realizePos_of_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {z : γ} (h : z ≠ d.newVertex) : d.realizePos R t z = R.pos z

theorem Schoenflies.CellStructure.SubdivData.realizePos_of_mem_cells {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {z : γ} (h : z ∈ S.cells) : d.realizePos R t z = R.pos z

theorem Schoenflies.CellStructure.SubdivData.realizePos_of_mem_vertexSet {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {z : γ} (h : z ∈ S.skel.vertexSet) : d.realizePos R t z = R.pos z

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeDrawing_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizeDrawing R t d.newEdge₁ = subarc (R.drawing d.edge) (d.leftParam R) t

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeDrawing_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizeDrawing R t d.newEdge₂ = subarc (R.drawing d.edge) t (d.rightParam R)

theorem Schoenflies.CellStructure.SubdivData.realizeDrawing_of_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} (h₁ : f ≠ d.newEdge₁) (h₂ : f ≠ d.newEdge₂) : d.realizeDrawing R t f = R.drawing f

theorem Schoenflies.CellStructure.SubdivData.realizeDrawing_of_mem_cells {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} (h : f ∈ S.cells) : d.realizeDrawing R t f = R.drawing f

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeCell_newVertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizeCell R t d.newVertex = {R.drawing d.edge t}

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeCell_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizeCell R t d.newEdge₁ = R.drawing d.edge '' Set.uIcc (d.leftParam R) t \ {R.pos d.left, R.drawing d.edge t}

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realizeCell_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizeCell R t d.newEdge₂ = R.drawing d.edge '' Set.uIcc t (d.rightParam R) \ {R.drawing d.edge t, R.pos d.right}

theorem Schoenflies.CellStructure.SubdivData.realizeCell_of_mem_cells {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {c : γ} (h : c ∈ S.cells) : d.realizeCell R t c = R.cell c

The two half arcs

theorem Schoenflies.CellStructure.SubdivData.edgeArc_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁ = R.drawing d.edge '' Set.uIcc (d.leftParam R) t

theorem Schoenflies.CellStructure.SubdivData.edgeArc_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂ = R.drawing d.edge '' Set.uIcc t (d.rightParam R)

theorem Schoenflies.CellStructure.SubdivData.edgeArc_of_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} (h₁ : f ≠ d.newEdge₁) (h₂ : f ≠ d.newEdge₂) : Graph.edgeArc (d.realizeDrawing R t) f = Graph.edgeArc R.drawing f

The two cell-shape fields of a realization

theorem Schoenflies.CellStructure.SubdivData.cell_vertex_realize {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} ⦃v : γ⦄ (hv : v ∈ d.skeleton.vertexSet) : d.realizeCell R t v = {d.realizePos R t v}

Every 0-cell of the subdivided structure is realized by its point.

theorem Schoenflies.CellStructure.SubdivData.cell_edge_realize {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} ⦃g x y : γ⦄ (hl : d.skeleton.IsLink g x y) : d.realizeCell R t g = Graph.edgeArc (d.realizeDrawing R t) g \ {d.realizePos R t x, d.realizePos R t y}

Every 1-cell of the subdivided structure is realized by its open arc.

theorem Schoenflies.CellStructure.SubdivData.injOn_realizePos {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Set.InjOn (d.realizePos R t) d.skeleton.vertexSet

Distinct 0-cells of the subdivided structure sit at distinct points: the new one is an interior point of a drawn edge, so it is none of the old ones.

theorem Schoenflies.CellStructure.SubdivData.edgeArc_newEdge₁_subset {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁ ⊆ Graph.edgeArc R.drawing d.edge

theorem Schoenflies.CellStructure.SubdivData.edgeArc_newEdge₂_subset {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂ ⊆ Graph.edgeArc R.drawing d.edge

theorem Schoenflies.CellStructure.SubdivData.edgeArc_new_union {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁ ∪ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂ = Graph.edgeArc R.drawing d.edge

The two new arcs cover the old one.

theorem Schoenflies.CellStructure.SubdivData.edgeArc_new_inter {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁ ∩ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂ = {R.drawing d.edge t}

The two new arcs meet exactly at the new point.

theorem Schoenflies.CellStructure.SubdivData.posLeft_mem_edgeArc_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : R.pos d.left ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁

theorem Schoenflies.CellStructure.SubdivData.posRight_mem_edgeArc_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : R.pos d.right ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂

theorem Schoenflies.CellStructure.SubdivData.newPos_mem_edgeArc_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : R.drawing d.edge t ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁

theorem Schoenflies.CellStructure.SubdivData.newPos_mem_edgeArc_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : R.drawing d.edge t ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂

theorem Schoenflies.CellStructure.SubdivData.posRight_notMem_edgeArc_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : R.pos d.right ∉ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁

The far endpoint of the old edge misses the near half.

theorem Schoenflies.CellStructure.SubdivData.posLeft_notMem_edgeArc_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : R.pos d.left ∉ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂

theorem Schoenflies.CellStructure.SubdivData.newPos_notMem_edgeArc_of_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {f : γ} (hf : f ∈ S.skel.edgeSet) (hfe : f ≠ d.edge) : R.drawing d.edge t ∉ Graph.edgeArc R.drawing f

The new point lies on no old edge but the subdivided one.

The subdivided drawn skeleton

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_edgeSet {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : (d.realizeGraph R t).edgeSet = d.skeleton.edgeSet

theorem Schoenflies.CellStructure.SubdivData.realizePos_image_vertexSet {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : d.realizePos R t '' S.skel.vertexSet = R.pos '' S.skel.vertexSet

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_vertexSet {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : (d.realizeGraph R t).vertexSet = insert (R.drawing d.edge t) R.graph.vertexSet

theorem Schoenflies.CellStructure.SubdivData.mem_realizeGraph_vertexSet_of_mem {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {p : Plane} (hp : p ∈ R.graph.vertexSet) : p ∈ (d.realizeGraph R t).vertexSet

theorem Schoenflies.CellStructure.SubdivData.mem_edgeSet_skel_of_ne {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} (hf : f ∈ (d.realizeGraph R t).edgeSet) (h₁ : f ≠ d.newEdge₁) (h₂ : f ≠ d.newEdge₂) : f ∈ S.skel.edgeSet ∧ f ≠ d.edge

An edge of the subdivided drawn skeleton that is neither new is an old edge, and not the subdivided one.

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_isLink_old {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} {x y : Plane} (hf : f ∈ S.skel.edgeSet) (hfe : f ≠ d.edge) : (d.realizeGraph R t).IsLink f x y ↔ R.graph.IsLink f x y

For an old edge the two drawn skeleta have the same links.

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_inc_old {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f : γ} {p : Plane} (hf : f ∈ S.skel.edgeSet) (hfe : f ≠ d.edge) : (d.realizeGraph R t).Inc f p ↔ R.graph.Inc f p

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_isLink_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : (d.realizeGraph R t).IsLink d.newEdge₁ (R.pos d.left) (R.drawing d.edge t)

theorem Schoenflies.CellStructure.SubdivData.realizeGraph_isLink_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : (d.realizeGraph R t).IsLink d.newEdge₂ (R.drawing d.edge t) (R.pos d.right)

theorem Schoenflies.CellStructure.SubdivData.mem_edgeArc_newEdge₁_vertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {p : Plane} (hp : p ∈ (d.realizeGraph R t).vertexSet) (hpa : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁) : p = R.pos d.left ∨ p = R.drawing d.edge t

A vertex on the first new arc is one of its two ends.

theorem Schoenflies.CellStructure.SubdivData.mem_edgeArc_newEdge₂_vertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {p : Plane} (hp : p ∈ (d.realizeGraph R t).vertexSet) (hpa : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂) : p = R.drawing d.edge t ∨ p = R.pos d.right

A vertex on the second new arc is one of its two ends.

Where two edges of the subdivided drawing meet

theorem Schoenflies.CellStructure.SubdivData.edge_inter_new_new {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {p : Plane} (hp₁ : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁) (hp₂ : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂) : p ∈ (d.realizeGraph R t).vertexSet ∧ (d.realizeGraph R t).Inc d.newEdge₁ p ∧ (d.realizeGraph R t).Inc d.newEdge₂ p

The two new edges meet exactly at the new vertex.

theorem Schoenflies.CellStructure.SubdivData.edge_inter_newEdge₁_old {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {g : γ} (hg : g ∈ S.skel.edgeSet) (hge : g ≠ d.edge) {p : Plane} (hp₁ : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁) (hpg : p ∈ Graph.edgeArc (d.realizeDrawing R t) g) : p ∈ (d.realizeGraph R t).vertexSet ∧ (d.realizeGraph R t).Inc d.newEdge₁ p ∧ (d.realizeGraph R t).Inc g p

The first new edge meets an old edge only at the position of d.left.

theorem Schoenflies.CellStructure.SubdivData.edge_inter_newEdge₂_old {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) {g : γ} (hg : g ∈ S.skel.edgeSet) (hge : g ≠ d.edge) {p : Plane} (hp₂ : p ∈ Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂) (hpg : p ∈ Graph.edgeArc (d.realizeDrawing R t) g) : p ∈ (d.realizeGraph R t).vertexSet ∧ (d.realizeGraph R t).Inc d.newEdge₂ p ∧ (d.realizeGraph R t).Inc g p

The second new edge meets an old edge only at the position of d.right.

theorem Schoenflies.CellStructure.SubdivData.edge_inter_old_old {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {f g : γ} (hf : f ∈ S.skel.edgeSet) (hfe : f ≠ d.edge) (hg : g ∈ S.skel.edgeSet) (hge : g ≠ d.edge) (hfg : f ≠ g) {p : Plane} (hpf : p ∈ Graph.edgeArc (d.realizeDrawing R t) f) (hpg : p ∈ Graph.edgeArc (d.realizeDrawing R t) g) : p ∈ (d.realizeGraph R t).vertexSet ∧ (d.realizeGraph R t).Inc f p ∧ (d.realizeGraph R t).Inc g p

Two old edges meet where they met before.

The subdivided drawing

theorem Schoenflies.CellStructure.SubdivData.isDrawing_realize {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realizeGraph R t).IsDrawing (d.realizeDrawing R t)

The subdivided data really is a drawing.

The two new open edges, as arcs

theorem Schoenflies.CellStructure.SubdivData.isArcBetween_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : IsArcBetween (Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁) (R.pos d.left) (R.drawing d.edge t)

The first new edge is drawn as an arc from the position of d.left to the new point.

theorem Schoenflies.CellStructure.SubdivData.isArcBetween_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : IsArcBetween (Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂) (R.drawing d.edge t) (R.pos d.right)

The second new edge is drawn as an arc from the new point to the position of d.right.

The realization of the subdivided structure

noncomputable def Schoenflies.CellStructure.SubdivData.realize {γ : Type u_2} {S : CellStructure γ} (d : S.SubdivData) (R : S.Realization) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) : (S.subdivideEdge d).Realization

The realization of an edge subdivision. The new 0-cell goes to the point of the drawn edge at parameter t, the two new 1-cells are drawn by the two halves of that parametrization, and every surviving cell is exactly where it was.

There is no geometric side condition: everything the construction needs is already carried by R, and is extracted by the lemmas above rather than assumed.

Equations

• d.realize R t ht = { pos := d.realizePos R t, drawing := d.realizeDrawing R t, injOn_pos := ⋯, isDrawing := ⋯, cell := d.realizeCell R t, cell_vertex := ⋯, cell_edge := ⋯ }

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realize_pos {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realize R t ht).pos = d.realizePos R t

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realize_drawing {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realize R t ht).drawing = d.realizeDrawing R t

@[simp]

theorem Schoenflies.CellStructure.SubdivData.realize_cell {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realize R t ht).cell = d.realizeCell R t

The realization refines the old one

theorem Schoenflies.CellStructure.SubdivData.closure_realizeCell_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : closure (d.realizeCell R t d.newEdge₁) = Graph.edgeArc (d.realizeDrawing R t) d.newEdge₁

theorem Schoenflies.CellStructure.SubdivData.closure_realizeCell_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : closure (d.realizeCell R t d.newEdge₂) = Graph.edgeArc (d.realizeDrawing R t) d.newEdge₂

theorem Schoenflies.CellStructure.SubdivData.realizeCell_edge_eq {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : R.cell d.edge = d.realizeCell R t d.newEdge₁ ∪ d.realizeCell R t d.newVertex ∪ d.realizeCell R t d.newEdge₂

The old open edge is cut into the two new open edges and the new 0-cell.

theorem Schoenflies.CellStructure.SubdivData.nonempty_realizeCell_newEdge₁ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realizeCell R t d.newEdge₁).Nonempty

theorem Schoenflies.CellStructure.SubdivData.nonempty_realizeCell_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realizeCell R t d.newEdge₂).Nonempty

theorem Schoenflies.CellStructure.SubdivData.disjoint_newEdge₁_newVertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : Disjoint (d.realizeCell R t d.newEdge₁) (d.realizeCell R t d.newVertex)

theorem Schoenflies.CellStructure.SubdivData.disjoint_newEdge₂_newVertex {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} : Disjoint (d.realizeCell R t d.newEdge₂) (d.realizeCell R t d.newVertex)

theorem Schoenflies.CellStructure.SubdivData.disjoint_newEdge₁_newEdge₂ {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : Disjoint (d.realizeCell R t d.newEdge₁) (d.realizeCell R t d.newEdge₂)

theorem Schoenflies.CellStructure.SubdivData.isRefinement_realize {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : d.IsRefinement R (d.realize R t ht)

The subdivided realization refines the given one — every field of SubdivData.IsRefinement. With IsRefinement.isCellDecomposition_and_isFaceJordan this hands a consumer IsCellDecomposition, IsFaceJordan and Refines at the new stage.

theorem Schoenflies.CellStructure.SubdivData.realize_isCellDecomposition_and_isFaceJordan {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) (hS : S.CombInvariants) {D : Set Plane} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : (d.realize R t ht).IsCellDecomposition D ∧ (d.realize R t ht).IsFaceJordan ∧ (d.realize R t ht).Refines R d.parent

The whole induction step over the first constructor, constructed. One edge subdivision of a realization satisfying (i) and (vii) produces a realization satisfying (i) and (vii) and refining it, constructing the refined realization in the conclusion.

The subdivision does not move the skeleton

Cutting an edge in two adds a point that was already on the drawing and replaces one arc by two whose union is that arc. So the realized 1-skeleton is literally the same set — which is what lets a skeleton homeomorphism be transported across a subdivision without being rebuilt.

theorem Schoenflies.CellStructure.SubdivData.pointSet_realize {t : ℝ} {γ : Type u_2} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} (ht : t ∈ Set.Ioo 0 1) : (d.realizeGraph R t).pointSet (d.realizeDrawing R t) = R.graph.pointSet R.drawing

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

An edge subdivision does not move the realized 1-skeleton.