Pairings in canonical normal-form words

This file classifies the directed polygonal identifications generated by both canonical boundary word families. The nonorientable generators are same-parameter crosscap pairings and opposite-parameter boundary-seam pairings. The orientable generators are opposite-parameter a-handle, b-handle, and boundary-seam pairings. Each pairing appears in both source/target orders. The free h dart in each boundary block occurs only once and contributes no gluing.

Nonorientable pairing instructions

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapIdentification {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (nonOrientableCellComplex p n).Face (nonOrientableCellComplex p n).faceBoundaryLength

The same-direction identification contributed by the square aᵢ aᵢ.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryIdentification {p n : ℕ} (j : Fin n) : PolygonGluing.Identification (nonOrientableCellComplex p n).Face (nonOrientableCellComplex p n).faceBoundaryLength

The opposite-direction identification contributed by cⱼ ... cⱼ⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapIdentificationReverse {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (nonOrientableCellComplex p n).Face (nonOrientableCellComplex p n).faceBoundaryLength

The reverse ordered direction of a crosscap identification.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryIdentificationReverse {p n : ℕ} (j : Fin n) : PolygonGluing.Identification (nonOrientableCellComplex p n).Face (nonOrientableCellComplex p n).faceBoundaryLength

The reverse ordered direction of a boundary-seam identification.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapPosition_zero_ne_one {p n : ℕ} (i : Fin p) : nonOrientableCrosscapPosition p n i 0 ≠ nonOrientableCrosscapPosition p n i 1

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryPosition_zero_ne_two {p n : ℕ} (j : Fin n) : nonOrientableBoundaryPosition p n j 0 ≠ nonOrientableBoundaryPosition p n j 2

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_edgeOccurrences_a {p n : ℕ} (i : Fin p) : SurfaceCellComplex.wordEdgeOccurrences (nonOrientableBoundaryWord p n) (NonOrientableEdge.a i) = {nonOrientableCrosscapPosition p n i 0, nonOrientableCrosscapPosition p n i 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_edgeOccurrences_c {p n : ℕ} (j : Fin n) : SurfaceCellComplex.wordEdgeOccurrences (nonOrientableBoundaryWord p n) (NonOrientableEdge.c j) = {nonOrientableBoundaryPosition p n j 0, nonOrientableBoundaryPosition p n j 2}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_edgeOccurrences_h {p n : ℕ} (j : Fin n) : SurfaceCellComplex.wordEdgeOccurrences (nonOrientableBoundaryWord p n) (NonOrientableEdge.h j) = {nonOrientableBoundaryPosition p n j 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapIdentification_mem {p n : ℕ} (hp : 1 ≤ p) (i : Fin p) : nonOrientableCrosscapIdentification i ∈ (nonOrientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryIdentification_mem {p n : ℕ} (hp : 1 ≤ p) (j : Fin n) : nonOrientableBoundaryIdentification j ∈ (nonOrientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapIdentificationReverse_mem {p n : ℕ} (hp : 1 ≤ p) (i : Fin p) : nonOrientableCrosscapIdentificationReverse i ∈ (nonOrientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryIdentificationReverse_mem {p n : ℕ} (hp : 1 ≤ p) (j : Fin n) : nonOrientableBoundaryIdentificationReverse j ∈ (nonOrientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.mem_nonOrientable_polygonalIdentifications_iff {p n : ℕ} (hp : 1 ≤ p) (identification : PolygonGluing.Identification (nonOrientableCellComplex p n).Face (nonOrientableCellComplex p n).faceBoundaryLength) : identification ∈ (nonOrientableCellComplex p n).polygonalIdentifications ⋯ ↔ (∃ (i : Fin p), identification = nonOrientableCrosscapIdentification i ∨ identification = nonOrientableCrosscapIdentificationReverse i) ∨ ∃ (j : Fin n), identification = nonOrientableBoundaryIdentification j ∨ identification = nonOrientableBoundaryIdentificationReverse j

Every directed polygonal identification in the canonical nonorientable word is one of the two ordered directions of an aᵢ or cⱼ generator.

Orientable pairing instructions

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandlePosition_zero_ne_two {p n : ℕ} (i : Fin p) : orientableHandlePosition p n i 0 ≠ orientableHandlePosition p n i 2

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandlePosition_one_ne_three {p n : ℕ} (i : Fin p) : orientableHandlePosition p n i 1 ≠ orientableHandlePosition p n i 3

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryPosition_zero_ne_two {p n : ℕ} (j : Fin n) : orientableBoundaryPosition p n j 0 ≠ orientableBoundaryPosition p n j 2

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_edgeOccurrences_a {p n : ℕ} (i : Fin p) : SurfaceCellComplex.wordEdgeOccurrences (orientableBoundaryWord p n) (OrientableEdge.a i) = {orientableHandlePosition p n i 0, orientableHandlePosition p n i 2}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_edgeOccurrences_b {p n : ℕ} (i : Fin p) : SurfaceCellComplex.wordEdgeOccurrences (orientableBoundaryWord p n) (OrientableEdge.b i) = {orientableHandlePosition p n i 1, orientableHandlePosition p n i 3}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_edgeOccurrences_c {p n : ℕ} (j : Fin n) : SurfaceCellComplex.wordEdgeOccurrences (orientableBoundaryWord p n) (OrientableEdge.c j) = {orientableBoundaryPosition p n j 0, orientableBoundaryPosition p n j 2}

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_edgeOccurrences_h {p n : ℕ} (j : Fin n) : SurfaceCellComplex.wordEdgeOccurrences (orientableBoundaryWord p n) (OrientableEdge.h j) = {orientableBoundaryPosition p n j 1}

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleAIdentification {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The opposite-direction identification contributed by aᵢ ... aᵢ⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleBIdentification {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The opposite-direction identification contributed by bᵢ ... bᵢ⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryIdentification {p n : ℕ} (j : Fin n) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The opposite-direction identification contributed by cⱼ ... cⱼ⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleAIdentificationReverse {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The reverse ordered direction of an orientable aᵢ identification.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleBIdentificationReverse {p n : ℕ} (i : Fin p) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The reverse ordered direction of an orientable bᵢ identification.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryIdentificationReverse {p n : ℕ} (j : Fin n) : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength

The reverse ordered direction of an orientable boundary-seam identification.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleAIdentification_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (i : Fin p) : orientableHandleAIdentification i ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleBIdentification_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (i : Fin p) : orientableHandleBIdentification i ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryIdentification_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (j : Fin n) : orientableBoundaryIdentification j ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleAIdentificationReverse_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (i : Fin p) : orientableHandleAIdentificationReverse i ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleBIdentificationReverse_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (i : Fin p) : orientableHandleBIdentificationReverse i ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryIdentificationReverse_mem {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (j : Fin n) : orientableBoundaryIdentificationReverse j ∈ (orientableCellComplex p n).polygonalIdentifications ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.mem_orientable_polygonalIdentifications_iff {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) (identification : PolygonGluing.Identification (orientableCellComplex p n).Face (orientableCellComplex p n).faceBoundaryLength) : identification ∈ (orientableCellComplex p n).polygonalIdentifications ⋯ ↔ (∃ (i : Fin p), identification = orientableHandleAIdentification i ∨ identification = orientableHandleAIdentificationReverse i) ∨ (∃ (i : Fin p), identification = orientableHandleBIdentification i ∨ identification = orientableHandleBIdentificationReverse i) ∨ ∃ (j : Fin n), identification = orientableBoundaryIdentification j ∨ identification = orientableBoundaryIdentificationReverse j

Every directed polygonal identification in the canonical orientable word is one of the two ordered directions of an aᵢ, bᵢ, or cⱼ generator.