Cancellation chains for finite cyclic presentations

This file implements Gallier--Xu Step 1. The exact base spelling has a fresh-last edge followed immediately by its inverse. Splitting between that pair and the remaining word produces exactly the P1 expansion of the one-sided split of the word with the pair removed. Thus one P2 split, one P1 contraction, and one one-sided P2 merge cancel the pair.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.target {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The word after deleting the displayed inverse pair.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.target X = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace X

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.source {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The base cancellation spelling, with the cancellable edge named last.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.retainWord_contractWord_of_fresh_not_mem {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hfresh : P1.freshEdge n ∉ List.map edgeOfDart word) : P2.retainWord (P1.contractWord word) = word

Retaining after contraction recovers a word which does not use the fresh-last edge.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.moveToLast {n : ℕ} (a : Fin (n + 1)) : Fin (n + 1) ≃ Fin (n + 1)

Move a chosen edge name to the fresh-last position.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.moveToLast a = Equiv.swap a (Fin.last n)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.renamedTail {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Rename a tail so that the displayed cancellable edge becomes last.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.lowerTail {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : List (SurfaceCellComplex.SignedDart (Fin n))

Delete the now-unused last edge name from a renamed tail.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.freshEdge_not_mem_renamedTail {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) : P1.freshEdge n ∉ List.map edgeOfDart (renamedTail a X)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.retainWord_lowerTail {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) : P2.retainWord (lowerTail a X) = renamedTail a X

Lowering and re-embedding a tail which avoids the cancellable edge recovers its exact renamed spelling.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.namedSource {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : FiniteCyclicPresentation

A one-face word with a displayed positive inverse pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.namedSourceSignedIso {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) : (namedSource a X).SignedPresentationIso (source (lowerTail a X))

Rename a displayed cancellable edge to last and contract the unused name from its tail.

Equations

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

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

Split the inverse pair from the remaining word.

Equations

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

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

Split the target at position zero, producing a monogon and the target word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.sourceCut_left {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : (sourceCut X).left = [SurfaceCellComplex.SignedDart.pos (P1.freshEdge n)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.sourceCut_right {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : (sourceCut X).right = [SurfaceCellComplex.SignedDart.neg (P1.freshEdge n)] ++ P2.retainWord X

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.targetCut_left {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut X).left = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.targetCut_right {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut X).right = X

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.expandWord_retainWord_fresh {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : P1.expandWord (P1.freshEdge n) (P2.retainWord X) = P2.retainWord (P2.retainWord X)

Expanding at the fresh-last edge only retains every twice-embedded old dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.split_source_eq_expand_split_target {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) : P2.split (source X) (sourceCut X) = P1.expand (P2.split (target X) (targetCut X)) (P2.freshEdge (target X))

The source split is exactly the P1 expansion of the target's one-sided split.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.target_isSurfaceValid {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (hX : X ≠ []) (validSource : (source X).IsSurfaceValid) : (target X).IsSurfaceValid

Deleting an inverse pair preserves the unoriented edge-occurrence multiplicities of all remaining edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.normalizationEquivalent {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (hX : X ≠ []) (validSource : (source X).IsSurfaceValid) : NormalizationEquivalent { presentation := source X, valid := validSource } { presentation := target X, valid := ⋯ }

Gallier--Xu Step 1 for the base spelling: split the inverse pair, contract the resulting two-edge paths, then merge the monogon produced by the one-sided target split.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.sphereNormalizationEquivalent (validSource : (source []).IsSurfaceValid) : NormalizationEquivalent { presentation := source [], valid := validSource } { presentation := twoMonogonSphere, valid := twoMonogonSphere_isSurfaceValid }

The zero-tail cancellation branch lands at the ordinary two-monogon sphere.

Cancellation in a multi-face context

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.target {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : FiniteCyclicPresentation

Delete the displayed pair in the first face and retain all other faces.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.target X W = { edgeCount := n, faces := X :: W }

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.source {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : FiniteCyclicPresentation

The base contextual cancellation spelling, with the cancellable edge named last.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.sourceCut {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source X W).P2Cut

Split the displayed inverse pair from the rest of the first source face.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.targetCut {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (target X W).P2Cut

Split the first target face at position zero.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.sourceCut_left {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (sourceCut X W).left = [SurfaceCellComplex.SignedDart.pos (P1.freshEdge n)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.sourceCut_right {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (sourceCut X W).right = [SurfaceCellComplex.SignedDart.neg (P1.freshEdge n)] ++ P2.retainWord X

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.sourceCut_isNondegenerate {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (sourceCut X W).IsNondegenerate

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.targetCut_left {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (targetCut X W).left = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.targetCut_right {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (targetCut X W).right = X

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.baseFaceEquiv {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source X W).Face ≃ (target X W).Face

Source and target retain the same face positions before the auxiliary P2 splits.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.baseFaceEquiv X W = finCongr ⋯

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.middleFaceEquiv {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (P2.split (source X W) (sourceCut X W)).Face ≃ (P1.expand (P2.split (target X W) (targetCut X W)) (P2.freshEdge (target X W))).Face

The face positions in the source split and the expanded target split have the same explicit indexing: old positions first and the right child last.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.middleFaceEquiv_apply_val {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (f : (P2.split (source X W) (sourceCut X W)).Face) : ↑((middleFaceEquiv X W) f) = ↑f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.middleFaceEquiv_oldFace {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (f : (source X W).Face) : (middleFaceEquiv X W) (P2.oldFace (source X W) (sourceCut X W) f) = (P1.faceEquiv (P2.split (target X W) (targetCut X W)) (P2.freshEdge (target X W))) (P2.oldFace (target X W) (targetCut X W) ((baseFaceEquiv X W) f))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.middleFaceEquiv_rightFace {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (middleFaceEquiv X W) (P2.rightFace (source X W) (sourceCut X W)) = (P1.faceEquiv (P2.split (target X W) (targetCut X W)) (P2.freshEdge (target X W))) (P2.rightFace (target X W) (targetCut X W))

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.splitSourceSignedIsoExpandSplitTarget {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (P2.split (source X W) (sourceCut X W)).SignedPresentationIso (P1.expand (P2.split (target X W) (targetCut X W)) (P2.freshEdge (target X W)))

Splitting the contextual source is signed-isomorphic to P1 expansion of the one-sided target split. Untouched faces are retained through both fresh-edge embeddings.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.normalizationEquivalent {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hX : X ≠ []) (validSource : (source X W).IsSurfaceValid) (validTarget : (target X W).IsSurfaceValid) : NormalizationEquivalent { presentation := source X W, valid := validSource } { presentation := target X W, valid := validTarget }

Gallier--Xu Step 1 inside a multi-face context: split the displayed pair, contract the resulting two-edge paths, and merge the monogon, leaving all other faces untouched.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.polygonallyEquivalent {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hX : X ≠ []) (validSource : (source X W).IsSurfaceValid) (validTarget : (target X W).IsSurfaceValid) : (source X W).PolygonallyEquivalent (target X W) validSource validTarget

Public realization-invariance form of contextual inverse-pair cancellation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.Context.normalizationEquivalentOfSignedIsos {P Q : FiniteCyclicPresentation} {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hX : X ≠ []) (sourceIso : P.SignedPresentationIso (source X W)) (targetIso : (target X W).SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := Q, valid := validQ }

Transport contextual cancellation across arbitrary edge names, face orders, orientations, and cyclic starting points supplied by signed presentation isomorphisms.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.normalizationEquivalentOfSignedIsos {P Q : FiniteCyclicPresentation} {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (hX : X ≠ []) (sourceIso : P.SignedPresentationIso (source X)) (targetIso : (target X).SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := Q, valid := validQ }

Transport base cancellation across arbitrary signed presentation isomorphisms. This is the stable constructor used after rotating a face and renaming its cancellable edge to the last index.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.polygonallyEquivalentOfSignedIsos {P Q : FiniteCyclicPresentation} {n : ℕ} (X : List (SurfaceCellComplex.SignedDart (Fin n))) (hX : X ≠ []) (sourceIso : P.SignedPresentationIso (source X)) (targetIso : (target X).SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonallyEquivalent Q validP validQ

Cancellation preserves faithful polygonal realization, in the transported public form.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.namedNormalizationEquivalent {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) (hlower : lowerTail a X ≠ []) (validSource : (namedSource a X).IsSurfaceValid) : NormalizationEquivalent { presentation := namedSource a X, valid := validSource } { presentation := target (lowerTail a X), valid := ⋯ }

Cancel a positively displayed adjacent inverse pair with an arbitrary edge name.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.negativeNamedSource {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : FiniteCyclicPresentation

A one-face word with a negatively displayed inverse pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.negativeNamedSourceSignedIso {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) : (negativeNamedSource a X).SignedPresentationIso (namedSource a X)

Reverse only the displayed edge to turn negative cancellation into positive cancellation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.negativeNamedNormalizationEquivalent {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) (hlower : lowerTail a X ≠ []) (validSource : (negativeNamedSource a X).IsSurfaceValid) : NormalizationEquivalent { presentation := negativeNamedSource a X, valid := validSource } { presentation := target (lowerTail a X), valid := ⋯ }

Cancel a negatively displayed adjacent inverse pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.normalizationEquivalentOfIsRotated {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hrotated : word ~r [SurfaceCellComplex.SignedDart.pos a, SurfaceCellComplex.SignedDart.neg a] ++ X) (ha : a ∉ List.map edgeOfDart X) (hlower : lowerTail a X ≠ []) (validSource : (Dyck.oneFace word).IsSurfaceValid) : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := validSource } { presentation := target (lowerTail a X), valid := ⋯ }

Cancel a positive adjacent inverse pair exposed by a cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.negativeNormalizationEquivalentOfIsRotated {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hrotated : word ~r [SurfaceCellComplex.SignedDart.neg a, SurfaceCellComplex.SignedDart.pos a] ++ X) (ha : a ∉ List.map edgeOfDart X) (hlower : lowerTail a X ≠ []) (validSource : (Dyck.oneFace word).IsSurfaceValid) : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := validSource } { presentation := target (lowerTail a X), valid := ⋯ }

Cancel a negative adjacent inverse pair exposed by a cyclic rotation.