Boundary cycles under the elementary cellulation operations

This module proves that the face-boundary invariant used to construct the two paths of an ear step is closed under face splitting and edge subdivision. The split proof is combinatorial: each new boundary is one old boundary arc followed by the reverse of the inserted ear.

Blueprint

• Schoenflies.CellStructure.SplitData.boundaryCycles — preservation under operation 2 of def:generated-structure.
• Schoenflies.CellStructure.SubdivData.boundaryCycles — preservation under operation 1.
• Schoenflies.GeneratedStructure.boundaryCycles — the closed induction.

theorem Schoenflies.CellStructure.SplitData.walkVertices_oldWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) : d.skeleton.walkVertices u W = S.skel.walkVertices u W

An old walk visits the same vertices when read in the enlarged skeleton.

theorem Schoenflies.CellStructure.SplitData.walkVertices_earWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.skeleton.walkVertices d.source d.earWalk = d.ear.vertexSet

The ear walk visits exactly the vertices of the abstract ear graph, even when read in the enlarged skeleton.

theorem Schoenflies.CellStructure.SplitData.walkVertices_reverse_earWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.skeleton.walkVertices d.target d.earWalk.reverse = d.ear.vertexSet

The reverse ear walk has the same vertex carrier.

theorem Schoenflies.CellStructure.SplitData.pathCells_oldWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) : (S.splitFace d).pathCells u W = S.pathCells u W

The cells of an old walk are unchanged in the enlarged skeleton.

theorem Schoenflies.CellStructure.SplitData.pathCells_earWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : (S.splitFace d).pathCells d.source d.earWalk = d.earCells

The cells of the ear walk, read in the enlarged skeleton, are exactly the cells of the abstract ear graph.

theorem Schoenflies.CellStructure.SplitData.pathCells_reverse_earWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : (S.splitFace d).pathCells d.target d.earWalk.reverse = d.earCells

Reversing the ear walk does not change its cell carrier.

theorem Schoenflies.CellStructure.SplitData.faceCycle_of_boundaryPath {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {newFace : γ} {P : List γ} (hface : newFace ∈ (S.splitFace d).faces) (hboundary : (S.splitFace d).boundary newFace = P ++ d.earWalk.reverse) (hP : S.skel.IsPath d.source P d.target) (hsub : ∀ ⦃σ : γ⦄, (S.splitFace d).sub σ newFace ↔ σ = newFace ∨ σ ∈ d.earCells ∨ σ ∈ S.pathCells d.source P) : Nonempty ((S.splitFace d).FaceCycle newFace)

One old boundary path closed by the reverse ear is a boundary cycle of a new face.

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

Face splitting preserves cyclic boundaries.

theorem Schoenflies.CellStructure.SubdivData.isPath_of_isWalk_of_isPath {γ : Type u_1} {G : Graph γ γ} {a b x y : γ} {W : List γ} (hP : G.IsPath a W b) (hW : G.IsWalk x W y) : G.IsPath x W y

A list which is a path in one orientation is a path in every orientation in which the same ordered edge list is a walk. The only alternative first orientation can occur for a single-edge path.

theorem Schoenflies.CellStructure.SubdivData.walkVertices_eq_of_notMem {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) (he : d.edge ∉ W) : d.skeleton.walkVertices u W = S.skel.walkVertices u W

A walk avoiding the subdivided edge visits exactly the same vertices in the subdivided skeleton.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.old_walkVertices_subset {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') : S.skel.walkVertices u W ⊆ d.skeleton.walkVertices u W'

Every old visited vertex is still visited after subdivision.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.new_walkVertices_subset {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') {z : γ} (hz : z ∈ d.skeleton.walkVertices u W') : z = d.newVertex ∨ z ∈ S.skel.walkVertices u W

A subdivision introduces no visited vertex except the named subdivision vertex.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.isPath {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u v : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (hP : S.skel.IsPath u W v) : d.skeleton.IsPath u W' v

Replacing one edge of a simple path by its two subdivision edges preserves simplicity.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.mem_input_of_mem_output {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') {x : γ} (hx : x ∈ W') : x = d.newEdge₁ ∨ x = d.newEdge₂ ∨ x ∈ W

Every output edge is either one of the two replacement edges or an old input edge.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.mem_output_of_mem_input_of_ne {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') {x : γ} (hx : x ∈ W) (hne : x ≠ d.edge) : x ∈ W'

Every surviving old input edge occurs in the output.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.edge_notMem_output {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') : d.edge ∉ W'

The removed edge name never occurs in the replacement list.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.newCells_subset_pathCells {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (he : d.edge ∈ W) : d.newCells ⊆ (S.subdivideEdge d).pathCells u W'

If the old walk crosses the subdivided edge, all three replacement cells occur in the new path carrier.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.pathCells_eq {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u v : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (hW : S.skel.IsWalk u W v) : (S.subdivideEdge d).pathCells u W' = {z : γ | z ∈ S.pathCells u W ∧ z ≠ d.edge ∨ d.edge ∈ W ∧ z ∈ d.newCells}

The exact cell-carrier update performed by an orientation-aware subdivision.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.exists_isCycleThrough {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W' : List γ} {e a b : γ} {D : List γ} (hsub : d.SubstWalk u (e :: D) W') (hW : S.skel.IsWalk u (e :: D) u) (hc : S.skel.IsCycleThrough e a b D) : ∃ (e' : γ) (a' : γ) (D' : List γ), W' = e' :: D' ∧ d.skeleton.IsCycleThrough e' a' u D'

Substituting an edge in a cyclic boundary list produces another presentation of a simple cycle, regardless of which admissible start vertex the boundary data selected.

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

Edge subdivision preserves cyclic boundaries.

The invariant at every generated stage

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

Every generated structure has cyclic face boundaries once the base structure does.