The Gallier--Xu Dyck rewrite

This file implements the common-subdivision identity underlying Gallier--Xu's handle extraction and boundary-loop grouping:

a U V a⁻¹ X ~ b V U b⁻¹ X.

We retain the edge name a for b. Both one-face words split to signed-isomorphic two-face presentations. The isomorphism exchanges the retained copy of a with the fresh cutting edge and reverses the former. The side words U, V, and X must not use a; this is exactly the side-condition available when the displayed two darts are the two occurrences of an inner edge.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A finite-cyclic presentation with one explicitly indexed face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace word = { edgeCount := n, faces := [word] }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace_boundary_zero {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (oneFace word).boundary 0 = word

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.source {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The source spelling of the Dyck rewrite.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.target {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A cyclic spelling of the target word a V U a⁻¹ X, chosen so its common P2 subdivision is definitionally transparent.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.sourceCut {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (source a U V X).P2Cut

The P2 cut of the source word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.targetCut {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (target a U V X).P2Cut

The P2 cut of the cyclic target spelling.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.sourceCut_isNondegenerate {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (sourceCut a U V X).IsNondegenerate

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.targetCut_isNondegenerate {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut a U V X).IsNondegenerate

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling {n : ℕ} (a : Fin n) : EdgeRelabeling (Fin (n + 1)) (Fin (n + 1))

Exchange the old edge a with the fresh P2 edge, reversing the old edge.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_pos_old {n : ℕ} (a : Fin n) : (commonEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.pos a.castSucc) = SurfaceCellComplex.SignedDart.neg (Fin.last n)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_neg_old {n : ℕ} (a : Fin n) : (commonEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.neg a.castSucc) = SurfaceCellComplex.SignedDart.pos (Fin.last n)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_pos_fresh {n : ℕ} (a : Fin n) : (commonEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.pos (Fin.last n)) = SurfaceCellComplex.SignedDart.pos a.castSucc

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_neg_fresh {n : ℕ} (a : Fin n) : (commonEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.neg (Fin.last n)) = SurfaceCellComplex.SignedDart.neg a.castSucc

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_castSucc_of_ne {n : ℕ} (a e : Fin n) (h : e ≠ a) (orientation : Bool) : (commonEdgeRelabeling a).mapDart (if orientation = true then SurfaceCellComplex.SignedDart.neg e.castSucc else SurfaceCellComplex.SignedDart.pos e.castSucc) = if orientation = true then SurfaceCellComplex.SignedDart.neg e.castSucc else SurfaceCellComplex.SignedDart.pos e.castSucc

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonEdgeRelabeling_retainWord {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (ha : a ∉ List.map edgeOfDart word) : List.map (commonEdgeRelabeling a).mapDart (P2.retainWord word) = P2.retainWord word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonFaceEquiv {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (target a U V X) (targetCut a U V X)).Face ≃ (P2.split (source a U V X) (sourceCut a U V X)).Face

Match the explicit face indices of the two canonical splits.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonFaceEquiv_selected {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (commonFaceEquiv a U V X) (P2.oldFace (target a U V X) (targetCut a U V X) 0) = P2.oldFace (source a U V X) (sourceCut a U V X) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.commonFaceEquiv_right {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (commonFaceEquiv a U V X) (P2.rightFace (target a U V X) (targetCut a U V X)) = P2.rightFace (source a U V X) (sourceCut a U V X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.split_target_boundary_selected {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (target a U V X) (targetCut a U V X)).boundary (P2.oldFace (target a U V X) (targetCut a U V X) 0) = P2.selectedBoundary (target a U V X) (targetCut a U V X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.split_source_boundary_selected {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (source a U V X) (sourceCut a U V X)).boundary (P2.oldFace (source a U V X) (sourceCut a U V X) 0) = P2.selectedBoundary (source a U V X) (sourceCut a U V X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.split_target_boundary_right {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (target a U V X) (targetCut a U V X)).boundary (P2.rightFace (target a U V X) (targetCut a U V X)) = P2.rightBoundary (target a U V X) (targetCut a U V X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.split_source_boundary_right {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (source a U V X) (sourceCut a U V X)).boundary (P2.rightFace (source a U V X) (sourceCut a U V X)) = P2.rightBoundary (source a U V X) (sourceCut a U V X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.map_selectedBoundary_isRotated {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) : List.map (commonEdgeRelabeling a).mapDart (P2.selectedBoundary (target a U V X) (targetCut a U V X)) ~r P2.selectedBoundary (source a U V X) (sourceCut a U V X)

The selected target child maps to a cyclic rotation of the selected source child.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.map_rightBoundary_isRotated {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) : List.map (commonEdgeRelabeling a).mapDart (P2.rightBoundary (target a U V X) (targetCut a U V X)) ~r P2.rightBoundary (source a U V X) (sourceCut a U V X)

The right target child maps to a cyclic rotation of the right source child.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.splitSignedPresentationIso {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) : (P2.split (target a U V X) (targetCut a U V X)).SignedPresentationIso (P2.split (source a U V X) (sourceCut a U V X))

The two canonical P2 splits in the Dyck rewrite differ only by signed edge relabeling.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.hasCommonSubdivision {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) : (source a U V X).HasCommonSubdivision (target a U V X)

The Gallier--Xu Dyck rewrite has a common directed subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.polygonallyEquivalent {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) (validSource : (source a U V X).IsSurfaceValid) (validTarget : (target a U V X).IsSurfaceValid) : (source a U V X).PolygonallyEquivalent (target a U V X) validSource validTarget

The Dyck rewrite preserves faithful polygonal realizations whenever the two displayed one-face presentations are ordinary-valid.