Polygonal realization under independently reoriented faces

Gallier--Xu treat a face and the same face read in the opposite direction interchangeably. This file records that convention explicitly. An UnorientedPresentationIso may rename and reorient edges, relabel faces, cyclically rotate their boundaries, and independently reverse the traversal orientation of every face.

Unlike SignedPresentationIso, this broader comparison does not claim to preserve the current orientation-sensitive IsSurfaceValid predicate. When both endpoints are ordinarily valid, it does preserve their faithful polygonal realizations. This is the exact extra comparison needed by the cross-cap pseudo-rewrite, whose common P2 refinement reads one of its two faces backwards.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reflectionHomeomorph (n : ℕ) : PolygonCell n ≃ₜ PolygonCell n

Reflection of a polygon cell across the real axis.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reflectionHomeomorph_apply (n : ℕ) (z : PolygonCell n) : ((reflectionHomeomorph n) z).val = (starRingEnd ℂ) z.val

theorem LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.reflectionHomeomorph_side {n : ℕ} (i : Fin n) (t : ↑unitInterval) : (reflectionHomeomorph n) ((side i) t) = (side i.rev) (unitInterval.symm t)

Reflection reverses both the cyclic side index and its interval parameter.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso (P Q : FiniteCyclicPresentation) : Type

Presentation isomorphism up to independent choices of traversal orientation on target faces.

• edgeRelabeling : EdgeRelabeling P.Edge Q.Edge

  The edgeRelabeling declaration.

• faceEquiv : P.Face ≃ Q.Face

  The faceEquiv declaration.

• reverseFace : P.Face → Bool

  The reverseFace declaration.

• boundary_rotated (f : P.Face) : List.map self.edgeRelabeling.mapDart (P.boundary f) ~r Q.orientedBoundary { face := self.faceEquiv f, orientation := self.reverseFace f }

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.edgeEquiv {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) : P.Edge ≃ Q.Edge

The edgeEquiv declaration.

Equations

• e.edgeEquiv = e.edgeRelabeling.edgeEquiv

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.ofSignedPresentationIso {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.UnorientedPresentationIso Q

Ordinary signed presentation isomorphisms are the orientation-preserving special case.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.boundary_length_eq {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) : (P.boundary f).length = (Q.boundary (e.faceEquiv f)).length

Corresponding stored boundaries have the same length.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.faceEdgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) (a : P.Edge) : P.faceEdgeMultiplicity f a = Q.faceEdgeMultiplicity (e.faceEquiv f) (e.edgeEquiv a)

Independent face reversal does not alter edge multiplicity in a corresponding face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.edgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (a : P.Edge) : P.edgeMultiplicity a = Q.edgeMultiplicity (e.edgeEquiv a)

Total edge multiplicities are invariant under an unoriented presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.isBoundaryEdge_iff {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (a : P.Edge) : P.IsBoundaryEdge a ↔ Q.IsBoundaryEdge (e.edgeEquiv a)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.map_faceAdjacent {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) {f g : P.Face} (h : P.FaceAdjacent f g) : Q.FaceAdjacent (e.faceEquiv f) (e.faceEquiv g)

Face adjacency is preserved when target faces may be read in either orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.isConnected {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (h : P.IsConnected) : Q.IsConnected

Face-incidence connectivity is preserved by an unoriented presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.inverseWord_get_rev {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) (i : Fin word.length) : (inverseWord word).get ⟨↑i, ⋯⟩ = (word.get i.rev).flip

Looking up the reversed signed word reverses the finite index and flips the dart.

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

The target-boundary rotation selected for an unoriented presentation isomorphism.

Equations

• e.faceRotation f = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.rotate_target_orientedBoundary {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) : (Q.orientedBoundary { face := e.faceEquiv f, orientation := e.reverseFace f }).rotate (e.faceRotation f) = List.map e.edgeRelabeling.mapDart (P.boundary f)

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.orientedSideIndex {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : Fin (Q.orientedBoundary { face := e.faceEquiv f, orientation := e.reverseFace f }).length

The side index in the chosen orientation of the target face.

Equations

• e.orientedSideIndex validQ f i = ⟨(↑i + e.faceRotation f) % (Q.orientedBoundary { face := e.faceEquiv f, orientation := e.reverseFace f }).length, ⋯⟩

@[reducible, inline]

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

Convert an oriented target-side index to the stored boundary indexing.

Equations

• e.sideIndex validQ f i = if e.reverseFace f = true then (Fin.cast ⋯ (e.orientedSideIndex validQ f i)).rev else Fin.cast ⋯ (e.orientedSideIndex validQ f i)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.sideParameter {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) (t : ↑unitInterval) : ↑unitInterval

Reflection reverses the side parameter exactly when the target face is read backwards.

Equations

• e.sideParameter f t = if e.reverseFace f = true then unitInterval.symm t else t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.sideParameter_false {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) (h : e.reverseFace f = false) (t : ↑unitInterval) : e.sideParameter f t = t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.sideParameter_true {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) (h : e.reverseFace f = true) (t : ↑unitInterval) : e.sideParameter f t = unitInterval.symm t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.sideParameter_sideParameter {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (f : P.Face) (t : ↑unitInterval) : e.sideParameter f (e.sideParameter f t) = t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.orientedBoundary_get_orientedSideIndex {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : (Q.orientedBoundary { face := e.faceEquiv f, orientation := e.reverseFace f }).get (e.orientedSideIndex validQ f i) = e.edgeRelabeling.mapDart ((P.boundary f).get i)

The rotated oriented target side carries the relabeled source dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.boundary_get_sideIndex {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) : (Q.boundary (e.faceEquiv f)).get (e.sideIndex validQ f i) = if e.reverseFace f = true then (e.edgeRelabeling.mapDart ((P.boundary f).get i)).flip else e.edgeRelabeling.mapDart ((P.boundary f).get i)

The stored target occurrence carries the relabeled dart, flipped exactly when its face was read backwards.

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

The facewise disk homeomorphism: rotate to the selected cyclic spelling, then reflect if the target face is read backwards.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.faceHomeomorph_side {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (f : P.Face) (i : Fin (P.boundary f).length) (t : ↑unitInterval) : (e.faceHomeomorph f) ((PolygonCell.side i) t) = (PolygonCell.side (e.sideIndex validQ f i)) (e.sideParameter f t)

The facewise homeomorphism sends a source side to the corresponding stored target side, with the interval parameter reversed exactly for a reversed face.

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

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.UnorientedPresentationIso.preHomeomorph_apply_fst {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (x : P.PolygonalPreRealization) : (e.preHomeomorph x).fst = e.faceEquiv x.fst

@[simp]

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

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

Transport a boundary occurrence through the selected cyclic rotation and possible reflection.

Equations

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

@[simp]

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.mapOccurrence_dart {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : P.BoundaryOccurrence) : (e.mapOccurrence validQ o).dart = if e.reverseFace o.fst = true then (e.edgeRelabeling.mapDart o.dart).flip else e.edgeRelabeling.mapDart o.dart

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

On a labelled side, the pre-realization map performs its selected cyclic shift and possible reflection.

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

Transport of all boundary occurrences is injective.

@[simp]

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

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

Ignoring the selected cyclic shifts and reflections, the occurrence types have equal cardinality.

Equations

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

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

Boundary-occurrence transport bundled as an equivalence.

Equations

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

@[simp]

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

@[simp]

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.transportDirection (sourceReverse targetReverse : Bool) : PolygonGluing.ParameterDirection → PolygonGluing.ParameterDirection

Toggle a gluing direction when exactly one incident face is reflected.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.transportDirection_parameter (sourceReverse targetReverse : Bool) (direction : PolygonGluing.ParameterDirection) (t : ↑unitInterval) : (transportDirection sourceReverse targetReverse direction).homeomorph (if sourceReverse = true then unitInterval.symm t else t) = if targetReverse = true then unitInterval.symm (direction.homeomorph t) else direction.homeomorph t

The transported gluing parameter commutes with the two optional side reflections.

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

Transport a compatible source pairing, toggling its parameter direction precisely when one of the two incident faces is reflected.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.mapPairing_direction {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) : (e.mapPairing validQ pairing).direction = transportDirection (e.reverseFace pairing.source.fst) (e.reverseFace pairing.target.fst) pairing.direction

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

The pre-realization map sends a pairing source point to its transported source side.

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

The pre-realization map sends a pairing target point to its transported target side.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.mapPairing_parameter_sideParameter {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : (e.mapPairing validQ pairing).identification.parameter (e.sideParameter pairing.source.fst t) = e.sideParameter pairing.target.fst (pairing.identification.parameter t)

Transported side parameters intertwine the source and target pairing maps.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_generator_related {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 generator into the target generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_related {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 generated gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_symm_occurrenceSide_point {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 (e.sideParameter ((e.occurrenceEquiv validQ).symm o).fst t)

The inverse pre-realization homeomorphism uses the same involutive side-parameter reflection.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.occurrenceEquiv_symm_mapDart {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (o : Q.BoundaryOccurrence) : e.edgeRelabeling.mapDart ((e.occurrenceEquiv validQ).symm o).dart = if e.reverseFace ((e.occurrenceEquiv validQ).symm o).fst = true then SurfaceCellComplex.SignedDart.flip o.dart else o.dart

The relabeled dart of a pulled-back occurrence is the target dart, flipped exactly when its source face was reflected.

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

The relabeled edge of a pulled-back occurrence is its target edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.comapPairing {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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.UnorientedPresentationIso.comapPairing_source {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) : (e.comapPairing validQ pairing).source = (e.occurrenceEquiv validQ).symm pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.comapPairing_target {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) : (e.comapPairing validQ pairing).target = (e.occurrenceEquiv validQ).symm pairing.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.comapPairing_direction {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) : (e.comapPairing validQ pairing).direction = transportDirection (e.reverseFace ((e.occurrenceEquiv validQ).symm pairing.source).fst) (e.reverseFace ((e.occurrenceEquiv validQ).symm pairing.target).fst) pairing.direction

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

The inverse pre-realization map sends a target pairing source to its pulled-back side.

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

The inverse pre-realization map sends a target pairing target to its pulled-back side.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.comapPairing_parameter_sideParameter {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso Q) (validQ : Q.IsSurfaceValid) (pairing : Q.BoundaryPairing) (t : ↑unitInterval) : (e.comapPairing validQ pairing).identification.parameter (e.sideParameter ((e.occurrenceEquiv validQ).symm pairing.source).fst t) = e.sideParameter ((e.occurrenceEquiv validQ).symm pairing.target).fst (pairing.identification.parameter t)

Pulled-back gluing parameters commute with the two side reflections.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_symm_generator_related {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 generated relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_symm_related {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 generated gluing relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.UnorientedPresentationIso.preHomeomorph_related_iff {P Q : FiniteCyclicPresentation} (e : P.UnorientedPresentationIso 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 facewise homeomorphism identifies the two generated gluing relations.

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

Independent edge and face reorientation preserves the faithful polygonal realization whenever both endpoint presentations satisfy ordinary incidence validity.

Equations

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

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

Propositional realization-invariance form for face-reversing presentation comparisons.