Realization of canonical finite-cyclic presentations

FiniteCyclicPresentation.ofOneFaceWord enumerates the edge names of an existing typed one-face word. This file proves that the enumeration does not change the faithful polygonal quotient. The result is the only adapter between the finite-cyclic normalization target and the already-certified canonical polygonal quotients; in particular, it does not restate either Lean-Eval relation.

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

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

The unique enumerated face is equivalent to the unique typed one-face face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordFaceHomeomorph {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (f : (ofOneFaceWord word).Face) : PolygonCell ((ofOneFaceWord word).boundary f).length ≃ₜ PolygonCell word.length

The face disk of the enumerated word, with its phantom side count cast back to the original word length.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordFaceHomeomorph word f = LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph ⋯ 0

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

Enumerating the edge names and the unique face leaves the polygonal pre-realization homeomorphic to the original typed one-face pre-realization.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_apply_fst {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (x : (ofOneFaceWord word).PolygonalPreRealization) : ((ofOneFaceWordPreHomeomorph word) x).fst = PUnit.unit

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_apply_snd {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (x : (ofOneFaceWord word).PolygonalPreRealization) : ((ofOneFaceWordPreHomeomorph word) x).snd = (ofOneFaceWordFaceHomeomorph word x.fst) x.snd

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

A boundary position of the enumerated word, read as the same position of the original typed word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapOccurrence word ⟨f, i⟩ = ⟨PUnit.unit, Fin.cast ⋯ i⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapOccurrence_fst {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (ofOneFaceWord word).BoundaryOccurrence) : (ofOneFaceWordMapOccurrence word o).fst = PUnit.unit

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapOccurrence_snd_val {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (ofOneFaceWord word).BoundaryOccurrence) : ↑(ofOneFaceWordMapOccurrence word o).snd = ↑o.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_occurrenceSide_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (ofOneFaceWord word).BoundaryOccurrence) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word) (((ofOneFaceWord word).occurrenceSide o).point t) = ((SurfaceCellComplex.oneFacePresentation Edge word).occurrenceSide (ofOneFaceWordMapOccurrence word o)).point t

The pre-realization homeomorphism is parameter-exact on every labelled side.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapOccurrence_dart {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (ofOneFaceWord word).BoundaryOccurrence) : (SurfaceCellComplex.SignedDart.mapEquiv (Fintype.equivFin Edge)) ((SurfaceCellComplex.oneFacePresentation Edge word).occurrenceDart (ofOneFaceWordMapOccurrence word o)) = o.dart

Relabeling the original dart at a mapped position recovers the enumerated dart exactly.

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

The inverse occurrence transport, from the typed one-face word to its enumeration.

Equations

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

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

Boundary positions are unchanged by enumeration.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordOccurrenceEquiv_apply {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (ofOneFaceWord word).BoundaryOccurrence) : (ofOneFaceWordOccurrenceEquiv word) o = ofOneFaceWordMapOccurrence word o

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapOccurrence_comap {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryOccurrence) : ofOneFaceWordMapOccurrence word ((ofOneFaceWordOccurrenceEquiv word).symm o) = o

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordComapOccurrence_dart {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryOccurrence) : (SurfaceCellComplex.SignedDart.mapEquiv (Fintype.equivFin Edge)) ((SurfaceCellComplex.oneFacePresentation Edge word).occurrenceDart o) = ((ofOneFaceWordOccurrenceEquiv word).symm o).dart

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid.not_isBoundaryEdge_of_distinct_occurrences {P : FiniteCyclicPresentation} (_valid : P.IsSurfaceValid) (source target : P.BoundaryOccurrence) (hne : source ≠ target) (hedge : target.edge = source.edge) : ¬P.IsBoundaryEdge source.edge

Two distinct occurrences of one finite-cyclic edge force that edge to be internal.

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

Transport a finite-cyclic pairing back to the original typed one-face word.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordComapPairing {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (valid : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) : (ofOneFaceWord word).BoundaryPairing

Pull a typed one-face pairing forward to the enumerated finite-cyclic word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapPairing_source {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) : (ofOneFaceWordMapPairing word pairing).source = ofOneFaceWordMapOccurrence word pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapPairing_target {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) : (ofOneFaceWordMapPairing word pairing).target = ofOneFaceWordMapOccurrence word pairing.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordMapPairing_direction {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) : (ofOneFaceWordMapPairing word pairing).direction = pairing.direction

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordComapPairing_source {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (valid : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) : (ofOneFaceWordComapPairing word valid pairing).source = (ofOneFaceWordOccurrenceEquiv word).symm pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordComapPairing_target {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (valid : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) : (ofOneFaceWordComapPairing word valid pairing).target = (ofOneFaceWordOccurrenceEquiv word).symm pairing.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordComapPairing_direction {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (valid : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) : (ofOneFaceWordComapPairing word valid pairing).direction = pairing.direction

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_pairing_source_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word) (pairing.identification.source.point t) = (ofOneFaceWordMapPairing word pairing).identification.source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_pairing_target_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word) (pairing.identification.target.point t) = (ofOneFaceWordMapPairing word pairing).identification.target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_pairing_parameter_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (pairing : (ofOneFaceWord word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word) (pairing.identification.target.point (pairing.identification.parameter t)) = (ofOneFaceWordMapPairing word pairing).identification.target.point ((ofOneFaceWordMapPairing word pairing).identification.parameter t)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_generator_related {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (_validFinite : (ofOneFaceWord word).IsSurfaceValid) (validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) (pairing : (ofOneFaceWord word).BoundaryPairing) (t : ↑unitInterval) : ((SurfaceCellComplex.oneFacePresentation Edge word).PolygonalGluingRel validTyped) ((ofOneFaceWordPreHomeomorph word) (pairing.identification.source.point t)) ((ofOneFaceWordPreHomeomorph word) (pairing.identification.target.point (pairing.identification.parameter t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_related {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) {x y : (ofOneFaceWord word).PolygonalPreRealization} (hxy : ((ofOneFaceWord word).PolygonalGluingRel validFinite) x y) : ((SurfaceCellComplex.oneFacePresentation Edge word).PolygonalGluingRel validTyped) ((ofOneFaceWordPreHomeomorph word) x) ((ofOneFaceWordPreHomeomorph word) y)

The enumeration pre-homeomorphism maps the complete finite-cyclic gluing relation into the typed one-face gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_occurrenceSide_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (o : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryOccurrence) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word).symm (((SurfaceCellComplex.oneFacePresentation Edge word).occurrenceSide o).point t) = ((ofOneFaceWord word).occurrenceSide ((ofOneFaceWordOccurrenceEquiv word).symm o)).point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_pairing_source_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word).symm (pairing.identification.source.point t) = (ofOneFaceWordComapPairing word validFinite pairing).identification.source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_pairing_target_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word).symm (pairing.identification.target.point t) = (ofOneFaceWordComapPairing word validFinite pairing).identification.target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_pairing_parameter_point {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) (t : ↑unitInterval) : (ofOneFaceWordPreHomeomorph word).symm (pairing.identification.target.point (pairing.identification.parameter t)) = (ofOneFaceWordComapPairing word validFinite pairing).identification.target.point ((ofOneFaceWordComapPairing word validFinite pairing).identification.parameter t)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_generator_related {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (_validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) (pairing : (SurfaceCellComplex.oneFacePresentation Edge word).BoundaryPairing) (t : ↑unitInterval) : ((ofOneFaceWord word).PolygonalGluingRel validFinite) ((ofOneFaceWordPreHomeomorph word).symm (pairing.identification.source.point t)) ((ofOneFaceWordPreHomeomorph word).symm (pairing.identification.target.point (pairing.identification.parameter t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_symm_related {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) {x y : (SurfaceCellComplex.oneFacePresentation Edge word).PolygonalPreRealization} (hxy : ((SurfaceCellComplex.oneFacePresentation Edge word).PolygonalGluingRel validTyped) x y) : ((ofOneFaceWord word).PolygonalGluingRel validFinite) ((ofOneFaceWordPreHomeomorph word).symm x) ((ofOneFaceWordPreHomeomorph word).symm y)

The inverse enumeration pre-homeomorphism maps the complete typed gluing relation back into the finite-cyclic gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordPreHomeomorph_related_iff {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) (x y : (ofOneFaceWord word).PolygonalPreRealization) : ((ofOneFaceWord word).PolygonalGluingRel validFinite) x y ↔ ((SurfaceCellComplex.oneFacePresentation Edge word).PolygonalGluingRel validTyped) ((ofOneFaceWordPreHomeomorph word) x) ((ofOneFaceWordPreHomeomorph word) y)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ofOneFaceWordRealizationHomeomorph {Edge : Type} [Fintype Edge] (word : List (SurfaceCellComplex.SignedDart Edge)) (validFinite : (ofOneFaceWord word).IsSurfaceValid) (validTyped : (SurfaceCellComplex.oneFacePresentation Edge word).OccurrencePairingValid) : (ofOneFaceWord word).PolygonalRealization validFinite ≃ₜ (SurfaceCellComplex.oneFacePresentation Edge word).PolygonalRealization validTyped

Enumerating the edge names of a typed one-face word preserves its faithful polygonal realization.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalOrientableRealizationHomeomorph {p n : ℕ} (hvalid : 1 ≤ p ∨ 1 ≤ n) : (orientable p n).canonicalPresentation.PolygonalRealization ⋯ ≃ₜ Quot (OrientableRel p n)

The admissible canonical orientable finite-cyclic presentation realizes the exact vendored Lean-Eval quotient.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalNonOrientableRealizationHomeomorph {p n : ℕ} (hp : 1 ≤ p) : (nonOrientable p n).canonicalPresentation.PolygonalRealization ⋯ ≃ₜ Quot (NonOrientableRel p n)

The admissible canonical nonorientable finite-cyclic presentation realizes the exact vendored Lean-Eval quotient.

Equations

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