Polygonal realization under signed presentation isomorphism

A signed presentation isomorphism may rename and independently reverse edge names, relabel faces, and cyclically rotate each stored face word. This file realizes those operations geometrically. The selected cyclic rotation acts on the circular polygon carrier by an exact complex rotation, so every labelled source side is sent to the target side carrying its relabelled dart.

The resulting homeomorphism of polygonal pre-realizations transports both the elementary gluing generators and their equivalence closures. It therefore descends to a homeomorphism of the faithful polygonal quotients.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotationUnit (n k : ℕ) : Circle

The rotationUnit declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotationUnit n k = Circle.exp (2 * Real.pi * ↑k / ↑n)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph {n m : ℕ} (h : n = m) (k : ℕ) : PolygonCell n ≃ₜ PolygonCell m

The rotateHomeomorph declaration.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph_apply_val {n m : ℕ} (h : n = m) (k : ℕ) (z : PolygonCell n) : ((rotateHomeomorph h k) z).val = ↑(rotationUnit n k) * z.val

def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateIndex {n : ℕ} (hn : 0 < n) (k : ℕ) (i : Fin n) : Fin n

The rotateIndex declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateIndex hn k i = ⟨(↑i + k) % n, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateIndex_val {n : ℕ} (hn : 0 < n) (k : ℕ) (i : Fin n) : ↑(rotateIndex hn k i) = (↑i + k) % n

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph_side {n : ℕ} (hn : 0 < n) (k : ℕ) (i : Fin n) (t : ↑unitInterval) : (rotateHomeomorph ⋯ k) ((side i) t) = (side (rotateIndex hn k i)) t

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph_side_of_eq {n m : ℕ} (h : n = m) (hm : 0 < m) (k : ℕ) (i : Fin n) (t : ↑unitInterval) : (rotateHomeomorph h k) ((side i) t) = (side ⟨(↑i + k) % m, ⋯⟩) t

Rotation sends a side to the correspondingly shifted side after changing only the phantom side-count index.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.faceRotation {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : ℕ

The target-boundary rotation selected for a signed presentation isomorphism.

Equations

• e.faceRotation f = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.rotate_target_boundary {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : (Q.boundary (e.faceEquiv f)).rotate (e.faceRotation f) = List.map e.edgeRelabeling.mapDart (P.boundary f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.sideIndex {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : Fin (Q.boundary (e.faceEquiv f)).length

The target side occupied by a source side after the selected face rotation.

Equations

• e.sideIndex validQ f i = ⟨(↑i + e.faceRotation f) % (Q.boundary (e.faceEquiv f)).length, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.sideIndex_val {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : ↑(e.sideIndex validQ f i) = (↑i + e.faceRotation f) % (Q.boundary (e.faceEquiv f)).length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.boundary_get_sideIndex {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : (Q.boundary (e.faceEquiv f)).get (e.sideIndex validQ f i) = e.edgeRelabeling.mapDart ((P.boundary f).get i)

The rotated target side carries exactly the relabeled source dart.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.faceHomeomorph {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : PolygonCell (P.boundary f).length ≃ₜ PolygonCell (Q.boundary (e.faceEquiv f)).length

The disk homeomorphism on a face selected by the cyclic boundary rotation.

Equations

• e.faceHomeomorph f = LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph ⋯ (e.faceRotation f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.PolygonalPreRealization ≃ₜ Q.PolygonalPreRealization

A signed presentation isomorphism gives a facewise homeomorphism of polygonal pre-realizations.

Equations

• e.preHomeomorph = IsHomeomorph.homeomorph (Sigma.map ⇑e.faceEquiv fun (f : P.Face) => ⇑(e.faceHomeomorph f)) ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_apply_fst {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (x : P.PolygonalPreRealization) : (e.preHomeomorph x).fst = e.faceEquiv x.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_apply_snd {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (x : P.PolygonalPreRealization) : (e.preHomeomorph x).snd = (e.faceHomeomorph x.fst) x.snd

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_side {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (t : ↑unitInterval) : e.preHomeomorph ⟨f, (PolygonCell.side i) t⟩ = ⟨e.faceEquiv f, (PolygonCell.side (e.sideIndex validQ f i)) t⟩

On a labelled side, the pre-realization homeomorphism is exactly the selected cyclic shift.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) : P.BoundaryOccurrence → Q.BoundaryOccurrence

Transport a boundary occurrence through the selected cyclic shift.

Equations

• e.mapOccurrence validQ ⟨f, i⟩ = ⟨e.faceEquiv f, e.sideIndex validQ f i⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_fst {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : (e.mapOccurrence validQ o).fst = e.faceEquiv o.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_snd_val {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : ↑(e.mapOccurrence validQ o).snd = (↑o.snd + e.faceRotation o.fst) % (Q.boundary (e.faceEquiv o.fst)).length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_dart {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : (e.mapOccurrence validQ o).dart = e.edgeRelabeling.mapDart o.dart

The transported occurrence carries the signed relabeling of the source dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_injective {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) : Function.Injective (e.mapOccurrence validQ)

Transport of boundary occurrences is injective.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_edge {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : (e.mapOccurrence validQ o).edge = e.edgeEquiv o.edge

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapPairing {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) : Q.BoundaryPairing

A compatible source pairing transports to a compatible target pairing.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapPairing_direction {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) : (e.mapPairing validQ pairing).direction = pairing.direction

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapPairing_source {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) : (e.mapPairing validQ pairing).source = e.mapOccurrence validQ pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapPairing_target {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) : (e.mapPairing validQ pairing).target = e.mapOccurrence validQ pairing.target

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_occurrenceSide_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) (t : ↑unitInterval) : e.preHomeomorph ((P.occurrenceSide o).point t) = (Q.occurrenceSide (e.mapOccurrence validQ o)).point t

The pre-realization homeomorphism maps an occurrence-side point to its transported side.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.rawOccurrenceEquiv {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.BoundaryOccurrence ≃ Q.BoundaryOccurrence

Ignoring cyclic shifts, corresponding boundary-occurrence types have the same cardinality.

Equations

• e.rawOccurrenceEquiv = e.faceEquiv.sigmaCongr fun (f : P.Face) => (Fin.castOrderIso ⋯).toEquiv

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.occurrenceEquiv {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) : P.BoundaryOccurrence ≃ Q.BoundaryOccurrence

The cyclic occurrence transport bundled as an equivalence.

Equations

• e.occurrenceEquiv validQ = Equiv.ofBijective (e.mapOccurrence validQ) ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.occurrenceEquiv_apply {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : (e.occurrenceEquiv validQ) o = e.mapOccurrence validQ o

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.mapOccurrence_occurrenceEquiv_symm {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : Q.BoundaryOccurrence) : e.mapOccurrence validQ ((e.occurrenceEquiv validQ).symm o) = o

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_occurrenceSide_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : Q.BoundaryOccurrence) (t : ↑unitInterval) : e.preHomeomorph.symm ((Q.occurrenceSide o).point t) = (P.occurrenceSide ((e.occurrenceEquiv validQ).symm o)).point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.occurrenceEquiv_symm_dart {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : Q.BoundaryOccurrence) : e.edgeRelabeling.mapDart ((e.occurrenceEquiv validQ).symm o).dart = o.dart

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.occurrenceEquiv_symm_edge {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : Q.BoundaryOccurrence) : e.edgeEquiv ((e.occurrenceEquiv validQ).symm o).edge = o.edge

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.comapPairing {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) : P.BoundaryPairing

Pull a compatible target pairing back through the occurrence equivalence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.comapPairing_direction {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) : (e.comapPairing validQ pairing).direction = pairing.direction

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_pairing_source_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph (pairing.identification.source.point t) = (e.mapPairing validQ pairing).identification.source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_pairing_target_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph (pairing.identification.target.point t) = (e.mapPairing validQ pairing).identification.target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_pairing_parameter_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph (pairing.identification.target.point (pairing.identification.parameter t)) = (e.mapPairing validQ pairing).identification.target.point ((e.mapPairing validQ pairing).identification.parameter t)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_generator_related {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (_validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : (Q.PolygonalGluingRel validQ) (e.preHomeomorph (pairing.identification.source.point t)) (e.preHomeomorph (pairing.identification.target.point (pairing.identification.parameter t)))

The facewise homeomorphism sends every source gluing generator into the target generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_related {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) {x y : P.PolygonalPreRealization} (hxy : (P.PolygonalGluingRel validP) x y) : (Q.PolygonalGluingRel validQ) (e.preHomeomorph x) (e.preHomeomorph y)

The facewise homeomorphism preserves the complete generated gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_pairing_source_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph.symm (pairing.identification.source.point t) = (e.comapPairing validQ pairing).identification.source.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_pairing_target_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph.symm (pairing.identification.target.point t) = (e.comapPairing validQ pairing).identification.target.point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_pairing_parameter_point {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) (t : ↑unitInterval) : e.preHomeomorph.symm (pairing.identification.target.point (pairing.identification.parameter t)) = (e.comapPairing validQ pairing).identification.target.point ((e.comapPairing validQ pairing).identification.parameter t)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_generator_related {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) (t : ↑unitInterval) : (P.PolygonalGluingRel validP) (e.preHomeomorph.symm (pairing.identification.source.point t)) (e.preHomeomorph.symm (pairing.identification.target.point (pairing.identification.parameter t)))

The inverse facewise homeomorphism sends every target generator into the source relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_symm_related {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) {x y : Q.PolygonalPreRealization} (hxy : (Q.PolygonalGluingRel validQ) x y) : (P.PolygonalGluingRel validP) (e.preHomeomorph.symm x) (e.preHomeomorph.symm y)

The inverse facewise homeomorphism preserves the complete generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.preHomeomorph_related_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) (x y : P.PolygonalPreRealization) : (P.PolygonalGluingRel validP) x y ↔ (Q.PolygonalGluingRel validQ) (e.preHomeomorph x) (e.preHomeomorph y)

The selected pre-realization homeomorphism identifies the two generated gluing relations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.realizationHomeomorph {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonalRealization validP ≃ₜ Q.PolygonalRealization validQ

Signed edge relabeling, face relabeling, and cyclic boundary rotation preserve the faithful polygonal realization.

Equations

• e.realizationHomeomorph validP validQ = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.realizationCongr e.preHomeomorph ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.polygonallyEquivalent {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonallyEquivalent Q validP validQ

Propositional realization-invariance form used by elementary-move closures.