Canonical finite cyclic presentations

This file fixes the finite-cyclic endpoint of the Gallier--Xu normalization lane. A typed one-face boundary word is enumerated by Fin exactly once, and the named normal forms use that adapter. The sphere branch uses the ordinary-valid two-monogon presentation obtained from the exceptional empty-word sphere by P2.

The orientable and nonorientable words remain the existing NormalForm.orientableBoundaryWord and NormalForm.nonOrientableBoundaryWord; this file does not introduce another formulation of the Lean-Eval representatives.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.map_edgeOfDart_eq_map_edgeName {Edge : Type} (word : List (SurfaceCellComplex.SignedDart Edge)) : List.map edgeOfDart word = List.map SurfaceCellComplex.SignedDart.edgeName word

The two existing projections from a signed dart to its unoriented edge agree.

@[reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) : FiniteCyclicPresentation

Enumerate the edge names of a typed one-face signed boundary word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_faces_length {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) : (ofOneFaceWord word).faces.length = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_boundary_zero {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) : (ofOneFaceWord word).boundary 0 = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv (Fintype.equivFin Edge))) word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_face_eq_zero {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (f : (ofOneFaceWord word).Face) : f = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_boundary {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (f : (ofOneFaceWord word).Face) : (ofOneFaceWord word).boundary f = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv (Fintype.equivFin Edge))) word

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordEdgeEquiv {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) : Edge ≃ (ofOneFaceWord word).Edge

The original edge names are equivalent to the enumerated one-face presentation edges.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordEdgeEquiv word = id (Fintype.equivFin Edge)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_edgeMultiplicity {Edge : Type} [Fintype Edge] [DecidableEq Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (e : Edge) : (ofOneFaceWord word).edgeMultiplicity ((ofOneFaceWordEdgeEquiv word) e) = List.count e (List.map edgeOfDart word)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_isSurfaceValid {Edge : Type} [Fintype Edge] [DecidableEq Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (hne : word ≠ []) (hmultiplicity : ∀ (e : Edge), List.count e (List.map edgeOfDart word) = 1 ∨ List.count e (List.map edgeOfDart word) = 2) : (ofOneFaceWord word).IsSurfaceValid

A nonempty typed one-face word with surface edge multiplicities gives an ordinary-valid finite cyclic presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWord_isConnected {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) : (ofOneFaceWord word).IsConnected

Every enumerated one-face presentation is connected at the face-incidence level.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation : NormalForm → FiniteCyclicPresentation

The single finite-cyclic target selected for each named normal form.

The admissibility predicate excludes the empty orientable word and the zero-crosscap nonorientable word when ordinary surface validity is required.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.sphere.canonicalPresentation = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_sphere : sphere.canonicalPresentation = FiniteCyclicPresentation.twoMonogonSphere

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_orientable (p n : ℕ) : (orientable p n).canonicalPresentation = FiniteCyclicPresentation.ofOneFaceWord (orientableBoundaryWord p n)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_nonOrientable (p n : ℕ) : (nonOrientable p n).canonicalPresentation = FiniteCyclicPresentation.ofOneFaceWord (nonOrientableBoundaryWord p n)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_isSurfaceValid (N : NormalForm) (hN : N.IsEvalAdmissible) : N.canonicalPresentation.IsSurfaceValid

Every Eval-admissible canonical presentation has ordinary surface incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_isConnected (N : NormalForm) : N.canonicalPresentation.IsConnected

Canonical finite-cyclic presentations are face-incidence connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalPresentation_isGallierValid (N : NormalForm) (hN : N.IsEvalAdmissible) : N.canonicalPresentation.IsGallierValid

Eval-admissible canonical presentations satisfy the packed Gallier--Xu input predicate.