Polygonal realization of finite cyclic presentations

This file gives FiniteCyclicPresentation a quotient-space semantics directly from its stored face words. A boundary occurrence is a face together with an index in that face's word, so repeated signed darts remain distinct polygon sides.

The pre-realization is the disjoint union of the standard polygonal disks indexed by the presentation's faces. Internal sides are paired exactly when their signed darts have the same underlying edge; equal signs use the same interval parameter and opposite signs use the reversed parameter.

FiniteCyclicPresentation.IsSurfaceValid already includes nonempty face boundaries, unlike the legacy cell-complex predicate. It therefore supplies the complete occurrence-pairing certificate needed by this construction.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryOccurrence (P : FiniteCyclicPresentation) : Type

A position in one of the stored cyclic face words.

Equations

• P.BoundaryOccurrence = ((f : P.Face) × Fin (P.boundary f).length)

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.boundaryOccurrenceFintype (P : FiniteCyclicPresentation) : Fintype P.BoundaryOccurrence

Equations

• P.boundaryOccurrenceFintype = inferInstance

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryOccurrence.dart {P : FiniteCyclicPresentation} (o : P.BoundaryOccurrence) : P.Dart

The signed dart stored at a boundary occurrence.

Equations

• o.dart = (P.boundary o.fst).get o.snd

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryOccurrence.edge {P : FiniteCyclicPresentation} (o : P.BoundaryOccurrence) : P.Edge

The unoriented edge stored at a boundary occurrence.

Equations

• o.edge = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart o.dart

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryOccurrence.dart_mk (P : FiniteCyclicPresentation) (f : P.Face) (i : Fin (P.boundary f).length) : (have this := ⟨f, i⟩; this).dart = (P.boundary f).get i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryOccurrence.edge_mk (P : FiniteCyclicPresentation) (f : P.Face) (i : Fin (P.boundary f).length) : (have this := ⟨f, i⟩; this).edge = edgeOfDart ((P.boundary f).get i)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.occurrenceSide (P : FiniteCyclicPresentation) (o : P.BoundaryOccurrence) : PolygonGluing.Side P.Face fun (f : P.Face) => (P.boundary f).length

The polygon side indexed by a boundary occurrence.

Equations

• P.occurrenceSide o = { face := o.fst, index := o.snd }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.occurrenceSide_face (P : FiniteCyclicPresentation) (o : P.BoundaryOccurrence) : (P.occurrenceSide o).face = o.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.occurrenceSide_index (P : FiniteCyclicPresentation) (o : P.BoundaryOccurrence) : (P.occurrenceSide o).index = o.snd

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOccurrences (P : FiniteCyclicPresentation) (e : P.Edge) : Finset P.BoundaryOccurrence

All boundary occurrences carrying the unoriented edge e.

Equations

• P.edgeOccurrences e = {o : P.BoundaryOccurrence | o.edge = e}

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.mem_edgeOccurrences (P : FiniteCyclicPresentation) (e : P.Edge) (o : P.BoundaryOccurrence) : o ∈ P.edgeOccurrences e ↔ o.edge = e

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeMultiplicity_eq_card_edgeOccurrences (P : FiniteCyclicPresentation) (e : P.Edge) : P.edgeMultiplicity e = (P.edgeOccurrences e).card

Total edge multiplicity is exactly the cardinality of the corresponding occurrence fiber.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.card_edgeOccurrences (P : FiniteCyclicPresentation) (e : P.Edge) : (P.edgeOccurrences e).card = P.edgeMultiplicity e

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.not_isBoundaryEdge_of_ne_of_edge_eq {P : FiniteCyclicPresentation} {o p : P.BoundaryOccurrence} (hop : o ≠ p) (hedge : p.edge = o.edge) : ¬P.IsBoundaryEdge o.edge

Two distinct occurrences of the same edge certify that the edge is internal.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing (P : FiniteCyclicPresentation) : Type

A compatible gluing instruction between two distinct internal boundary occurrences.

• source : P.BoundaryOccurrence

  The source declaration.

• target : P.BoundaryOccurrence

  The target declaration.

• source_ne_target : self.source ≠ self.target
• source_not_boundary : ¬P.IsBoundaryEdge self.source.edge
• target_not_boundary : ¬P.IsBoundaryEdge self.target.edge
• direction : PolygonGluing.ParameterDirection

  The direction declaration.

• compatible : match self.direction with | PolygonGluing.ParameterDirection.same => self.target.dart = self.source.dart | PolygonGluing.ParameterDirection.opposite => self.target.dart = SurfaceCellComplex.SignedDart.flip self.source.dart

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid.edgeMultiplicity_eq_two_of_not_boundary {P : FiniteCyclicPresentation} (h : P.IsSurfaceValid) {e : P.Edge} (he : ¬P.IsBoundaryEdge e) : P.edgeMultiplicity e = 2

A non-boundary edge of a valid presentation occurs exactly twice.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid.exists_unique_partner {P : FiniteCyclicPresentation} (h : P.IsSurfaceValid) (source : P.BoundaryOccurrence) (hsource : ¬P.IsBoundaryEdge source.edge) : ∃! target : P.BoundaryOccurrence, source ≠ target ∧ target.edge = source.edge

Every internal occurrence has a unique distinct partner carrying the same unoriented edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid.exists_pairing_source {P : FiniteCyclicPresentation} (h : P.IsSurfaceValid) (source : P.BoundaryOccurrence) (hsource : ¬P.IsBoundaryEdge source.edge) : ∃ (pairing : P.BoundaryPairing), pairing.source = source

Every internal boundary occurrence is the source of a compatible polygon-side pairing.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing.identification {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : PolygonGluing.Identification P.Face fun (f : P.Face) => (P.boundary f).length

The polygon-side identification associated to a compatible occurrence pairing.

Equations

• pairing.identification = { source := P.occurrenceSide pairing.source, target := P.occurrenceSide pairing.target, direction := pairing.direction }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing.identification_source {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : pairing.identification.source = P.occurrenceSide pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing.identification_target {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : pairing.identification.target = P.occurrenceSide pairing.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing.identification_direction {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : pairing.identification.direction = pairing.direction

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.polygonalIdentifications (P : FiniteCyclicPresentation) (_valid : P.IsSurfaceValid) : Set (PolygonGluing.Identification P.Face fun (f : P.Face) => (P.boundary f).length)

All polygon-side identifications compatible with a valid finite cyclic presentation.

Equations

• P.polygonalIdentifications _valid = Set.range LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.BoundaryPairing.identification

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.pairing_identification_mem {P : FiniteCyclicPresentation} (valid : P.IsSurfaceValid) (pairing : P.BoundaryPairing) : pairing.identification ∈ P.polygonalIdentifications valid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid.exists_identification_source {P : FiniteCyclicPresentation} (h : P.IsSurfaceValid) (source : P.BoundaryOccurrence) (hsource : ¬P.IsBoundaryEdge source.edge) : ∃ identification ∈ P.polygonalIdentifications h, identification.source = P.occurrenceSide source

Every internal occurrence of a valid presentation starts a prescribed identification.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonalPreRealization (P : FiniteCyclicPresentation) : Type

The disjoint union of the polygonal cells encoded by the stored face words.

Equations

• P.PolygonalPreRealization = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.PreRealization P.Face fun (f : P.Face) => (P.boundary f).length

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonalGluingRel (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) : Setoid P.PolygonalPreRealization

The generated relation from all compatible internal occurrence pairings.

Equations

• P.PolygonalGluingRel valid = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.setoid (P.polygonalIdentifications valid)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonalRealization (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) : Type

The polygonal quotient realized directly from a valid finite cyclic presentation.

Equations

• P.PolygonalRealization valid = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.Realization (P.polygonalIdentifications valid)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.polygonalMk (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) : P.PolygonalPreRealization → P.PolygonalRealization valid

The quotient map from the disjoint union of face polygons.

Equations

• P.polygonalMk valid = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.mk (P.polygonalIdentifications valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.continuous_polygonalMk (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) : Continuous (P.polygonalMk valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.isQuotientMap_polygonalMk (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) : Topology.IsQuotientMap (P.polygonalMk valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.polygonalMk_pairing_eq {P : FiniteCyclicPresentation} (valid : P.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : P.polygonalMk valid (pairing.identification.source.point t) = P.polygonalMk valid (pairing.identification.target.point (pairing.identification.parameter t))

Every compatible pairing identifies the corresponding side points in the quotient.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData (P Q : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : Type

Cut-and-paste data sufficient to compare two polygonal realizations.

The maps start on the two polygonal pre-realizations but land in the opposite quotient. This asymmetric-looking formulation is deliberate: after a polygon is cut into two faces, the reverse map need not lift continuously to the disjoint union of those faces, although it can be continuous as a map to their glued quotient.

• toPre : P.PolygonalPreRealization → Q.PolygonalRealization validQ

  The toPre declaration.

• invPre : Q.PolygonalPreRealization → P.PolygonalRealization validP

  The invPre declaration.

• continuous_toPre : Continuous self.toPre
• continuous_invPre : Continuous self.invPre
• to_respects (x y : P.PolygonalPreRealization) : (P.PolygonalGluingRel validP) x y → self.toPre x = self.toPre y
• inv_respects (x y : Q.PolygonalPreRealization) : (Q.PolygonalGluingRel validQ) x y → self.invPre x = self.invPre y
• left_inverse_mk (x : P.PolygonalPreRealization) : Quotient.lift self.invPre ⋯ (self.toPre x) = P.polygonalMk validP x
• right_inverse_mk (y : Q.PolygonalPreRealization) : Quotient.lift self.toPre ⋯ (self.invPre y) = Q.polygonalMk validQ y

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.toQuotient {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) : P.PolygonalRealization validP → Q.PolygonalRealization validQ

Descend the forward cut-and-paste map through the source gluing relation.

Equations

• data.toQuotient = Quotient.lift data.toPre ⋯

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.invQuotient {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) : Q.PolygonalRealization validQ → P.PolygonalRealization validP

Descend the reverse cut-and-paste map through the target gluing relation.

Equations

• data.invQuotient = Quotient.lift data.invPre ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.toQuotient_polygonalMk {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) (x : P.PolygonalPreRealization) : data.toQuotient (P.polygonalMk validP x) = data.toPre x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.invQuotient_polygonalMk {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) (y : Q.PolygonalPreRealization) : data.invQuotient (Q.polygonalMk validQ y) = data.invPre y

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.continuous_toQuotient {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) : Continuous data.toQuotient

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.continuous_invQuotient {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) : Continuous data.invQuotient

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.RealizationEquivData.homeomorph {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (data : P.RealizationEquivData Q validP validQ) : P.PolygonalRealization validP ≃ₜ Q.PolygonalRealization validQ

Cut-and-paste data descend to a homeomorphism of the generated polygonal quotients.

Equations

• data.homeomorph = { toFun := data.toQuotient, invFun := data.invQuotient, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonallyEquivalent (P Q : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : Prop

Quotient semantics for comparing two valid finite cyclic presentations.

Equations

• P.PolygonallyEquivalent Q validP validQ = Nonempty (P.PolygonalRealization validP ≃ₜ Q.PolygonalRealization validQ)

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

A cut-and-paste certificate proves polygonal equivalence.