Cyclic boundaries of abstract 2-cells

The abstract CellStructure.boundary field is only a list of edge names. The finite-transfer construction needs the stronger invariant that each face boundary is a simple cycle and that its vertices and edges are exactly the strict subcells of the face. This module packages that invariant in the representation already used by Graph.IsLongCycle.

The distinguished edge edge closes the simple detour walk. The list edge :: walk is a closed walk when started at target: it crosses the distinguished edge backwards to source and follows the detour back to target. Two-edge cycles are allowed: an ear split can legitimately create a digon even when the initial outer cycle has at least three vertices. Stating the carrier clause with CellStructure.pathCells makes it directly comparable with SplitData.sub_face.

Blueprint

• Schoenflies.CellStructure.FaceCycle, BoundaryCycles — the maintained form of the sentence in lem:cellulation-invariants that the cells below every 2-cell form its boundary cycle.

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

A face boundary is a simple cycle, and its carrier is exactly the face's strict subcells. This is data rather than a proposition because the finite-transfer step extracts its named edge, vertices and complementary path.

• face_mem : F ∈ S.faces

  The indexed cell is a face of the structure.

• edge : γ

  A distinguished edge of the boundary cycle.

• source : γ

  One end of the distinguished edge and the source of the complementary path.

• target : γ

  The other end, at which the displayed closed boundary list starts.

• walk : List γ

  The complementary path from source to target.

• boundary_eq : S.boundary F = self.edge :: self.walk

  The raw boundary datum is the distinguished edge followed by the complementary path.

• isCycle : S.skel.IsCycleThrough self.edge self.source self.target self.walk

  The distinguished edge and complementary path form a simple cycle.

• sub_face ⦃σ : γ⦄ : S.sub σ F ↔ σ = F ∨ σ ∈ S.pathCells self.target (self.edge :: self.walk)

  The face itself and the cells of the cycle are exactly the cells below the face.

structure Schoenflies.CellStructure.BoundaryPaths {γ : Type u_1} (S : CellStructure γ) (F a b : γ) : Type u_1

The two simple boundary paths obtained by cutting a face cycle at distinct vertices. Its last two fields are deliberately identical to SplitData.sub_face and SplitData.paths_meet, so an ear insertion can copy the data without translation.

• path₁ : List γ

  The first boundary path from a to b.

• path₂ : List γ

  The complementary boundary path.

• isPath₁ : S.skel.IsPath a self.path₁ b

  The first list is a simple path in the skeleton.

• isPath₂ : S.skel.IsPath a self.path₂ b

  The second list is a simple path in the skeleton.

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

  The face and the cells of the two paths are exactly the cells below the face.

• paths_meet : S.pathCells a self.path₁ ∩ S.pathCells a self.path₂ = {a, b}

  The paths meet only at their two endpoints.

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

Every 2-cell of an abstract structure admits simple boundary-cycle data. This is a proposition so that membership proofs remain proof-irrelevant; BoundaryCycles.faceCycle chooses the exported data once and for all.

• cycle (F : γ) : F ∈ S.faces → Nonempty (S.FaceCycle F)

  Existence of boundary-cycle data for each face.

noncomputable def Schoenflies.CellStructure.BoundaryCycles.faceCycle {γ : Type u_1} {S : CellStructure γ} (h : S.BoundaryCycles) (F : γ) (hF : F ∈ S.faces) : S.FaceCycle F

The chosen simple boundary cycle of a face.

Equations

• h.faceCycle F hF = Classical.choice ⋯

theorem Schoenflies.CellStructure.FaceCycle.isWalk {γ : Type u_1} {S : CellStructure γ} {F : γ} (h : S.FaceCycle F) : S.skel.IsWalk h.target (S.boundary F) h.target

The boundary list is a closed walk, in the orientation recorded by boundary_eq.

theorem Schoenflies.CellStructure.FaceCycle.sub_of_mem_pathCells {γ : Type u_1} {S : CellStructure γ} {F : γ} (h : S.FaceCycle F) {σ : γ} (hσ : σ ∈ S.pathCells h.target (h.edge :: h.walk)) : S.sub σ F

Every cell of the displayed boundary cycle is a strict subcell of its face.

theorem Schoenflies.CellStructure.FaceCycle.pathCells_append {γ : Type u_1} {S : CellStructure γ} {u w v : γ} {W₁ W₂ : List γ} (h₁ : S.skel.IsWalk u W₁ w) (h₂ : S.skel.IsWalk w W₂ v) : S.pathCells u (W₁ ++ W₂) = S.pathCells u W₁ ∪ S.pathCells w W₂

Path cells split over the concatenation of two composable walks.

theorem Schoenflies.CellStructure.FaceCycle.pathCells_reverse {γ : Type u_1} {S : CellStructure γ} {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) : S.pathCells v W.reverse = S.pathCells u W

Reversing a walk changes neither its edge cells nor its vertex cells.

theorem Schoenflies.CellStructure.FaceCycle.pathCells_eq_of_perm {γ : Type u_1} {S : CellStructure γ} {u₁ v₁ u₂ v₂ : γ} {W₁ W₂ : List γ} (h₁ : S.skel.IsWalk u₁ W₁ v₁) (h₂ : S.skel.IsWalk u₂ W₂ v₂) (hp : W₁.Perm W₂) (hne₁ : W₁ ≠ []) (hne₂ : W₂ ≠ []) : S.pathCells u₁ W₁ = S.pathCells u₂ W₂

Nonempty walks with permuted edge lists have the same path cells.

theorem Schoenflies.CellStructure.FaceCycle.mem_walk_of_vertex_sub {γ : Type u_1} {S : CellStructure γ} {F : γ} (h : S.FaceCycle F) {a : γ} (ha : a ∈ S.skel.vertexSet) (haF : S.sub a F) : a ∈ S.skel.walkVertices h.source h.walk

A vertex below a cyclic face lies on the complementary path used to present the cycle.

theorem Schoenflies.CellStructure.FaceCycle.boundaryPaths {γ : Type u_1} {S : CellStructure γ} {F : γ} (h : S.FaceCycle F) {a b : γ} (ha : a ∈ S.skel.vertexSet) (hb : b ∈ S.skel.vertexSet) (haF : S.sub a F) (hbF : S.sub b F) (hab : a ≠ b) : Nonempty (S.BoundaryPaths F a b)

Cutting a cyclic face at two distinct boundary vertices gives the two pieces required by SplitData. The second path returned by Graph.IsCycleThrough.split_at is reversed so that both displayed paths run from a to b.

noncomputable def Schoenflies.CellStructure.BoundaryCycles.boundaryPaths {γ : Type u_1} {S : CellStructure γ} (h : S.BoundaryCycles) (F : γ) (hF : F ∈ S.faces) (a b : γ) (ha : a ∈ S.skel.vertexSet) (hb : b ∈ S.skel.vertexSet) (haF : S.sub a F) (hbF : S.sub b F) (hab : a ≠ b) : S.BoundaryPaths F a b

The two chosen boundary paths between distinct vertices of a cyclic face.

Equations

• h.boundaryPaths F hF a b ha hb haF hbF hab = Classical.choice ⋯