The Gallier--Xu cross-cap rewrite

This file implements the common P2 refinement behind the pseudo-rewrite

a X a Y ~ b b Y⁻¹ X.

The first source child is compared in its stored orientation and the second source child is read backwards, exactly as in Gallier--Xu's derivation. The broader UnorientedPresentationIso makes that face-orientation choice explicit; it is not hidden in the ordinary signed edge relabeling.

@[reducible]

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

The source spelling with two equally oriented occurrences of a.

Equations

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

@[reducible]

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

A cyclic spelling of the target cross-cap word a a Y⁻¹ X.

Equations

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

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

Split the source between the two occurrences of a.

Equations

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

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

Split the target along the edge used to merge the first source child with the reverse of the second.

Equations

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

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

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

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

Exchange the target cross-cap edge with its fresh cutting edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.commonEdgeRelabeling a = { edgeEquiv := Equiv.swap a.castSucc (Fin.last n), reverse := fun (x : Fin (n + 1)) => false }

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

@[simp]

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.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.Crosscap.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.Crosscap.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.Crosscap.commonFaceEquiv {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (target a X Y) (targetCut a X Y)).Face ≃ (P2.split (source a X Y) (sourceCut a X Y)).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.Crosscap.commonFaceEquiv_selected {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (commonFaceEquiv a X Y) (P2.oldFace (target a X Y) (targetCut a X Y) 0) = P2.oldFace (source a X Y) (sourceCut a X Y) 0

@[simp]

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.reverseCommonFace {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (q : (P2.split (target a X Y) (targetCut a X Y)).Face) : Bool

Reverse exactly the right child of the target split.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.reverseCommonFace_selected {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : reverseCommonFace a X Y (P2.oldFace (target a X Y) (targetCut a X Y) 0) = false

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.reverseCommonFace_right {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : reverseCommonFace a X Y (P2.rightFace (target a X Y) (targetCut a X Y)) = true

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

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

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

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

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

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.map_rightBoundary_isRotated_inverse {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haY : a ∉ List.map edgeOfDart Y) : List.map (commonEdgeRelabeling a).mapDart (P2.rightBoundary (target a X Y) (targetCut a X Y)) ~r inverseWord (P2.rightBoundary (source a X Y) (sourceCut a X Y))

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.splitUnorientedPresentationIso {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) : (P2.split (target a X Y) (targetCut a X Y)).UnorientedPresentationIso (P2.split (source a X Y) (sourceCut a X Y))

The two P2 refinements differ by edge relabeling and reversal of their right child face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.polygonallyEquivalent {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) (validSource : (source a X Y).IsSurfaceValid) (validTarget : (target a X Y).IsSurfaceValid) : (source a X Y).PolygonallyEquivalent (target a X Y) validSource validTarget

The Gallier--Xu cross-cap rewrite preserves faithful polygonal realizations.