Polygonal realization of surface cell-complex data

This file connects face-boundary occurrences in SurfaceCellComplex to the generic quotient construction in PolygonalQuotient.lean. The distinction between occurrences and dart values is essential: a word such as a a has two different sides carrying the same oriented dart.

An internal pair carrying the same dart uses the identity interval parameter; a pair carrying inverse darts uses parameter reversal. OccurrencePairingValid combines the incidence-derived IsSurfaceValid predicate with the nonempty-boundary condition needed by the current polygon model. The public polygonal gluing relation requires a witness of this predicate.

SurfaceCellComplex.sphere uses the explicit two-monogon presentation needed by this polygonal realization, and the standard one-face examples have occurrence-validity witnesses. The adapter derives its orbit conditions from IsSurfaceValid.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.occurrenceDart (K : SurfaceCellComplex) (o : K.BoundaryOccurrence) : K.Dart

The oriented dart carried by a boundary occurrence.

Equations

• K.occurrenceDart o = o.dart

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.occurrenceSide (K : SurfaceCellComplex) (o : K.BoundaryOccurrence) : PolygonGluing.Side K.Face K.faceBoundaryLength

The polygon side indexed by a boundary occurrence.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.BoundaryPairing (K : SurfaceCellComplex) : Type

A compatible gluing instruction between two boundary occurrences.

Equal oriented darts use the same interval direction. Inverse darts use the opposite direction. Boundary darts are excluded from both ends of a gluing instruction.

• source : K.BoundaryOccurrence

  The source boundary occurrence in the pairing.

• target : K.BoundaryOccurrence

  The target boundary occurrence in the pairing.

• source_ne_target : self.source ≠ self.target
• source_not_boundary : ¬K.IsBoundaryDart (K.occurrenceDart self.source)
• target_not_boundary : ¬K.IsBoundaryDart (K.occurrenceDart self.target)
• direction : PolygonGluing.ParameterDirection

  Whether the gluing preserves or reverses the interval parameter.

• compatible : match self.direction with | PolygonGluing.ParameterDirection.same => K.occurrenceDart self.target = K.occurrenceDart self.source | PolygonGluing.ParameterDirection.opposite => K.occurrenceDart self.target = K.inv (K.occurrenceDart self.source)

structure LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid (K : SurfaceCellComplex) : Prop

Incidence validity together with nonempty face boundaries for the polygonal realization.

The extra boundary condition excludes the empty-word sphere presentation because PolygonCell 0 is a side-free disk, not a sphere. Connectedness and vertex-link conditions remain separate.

• surface_valid : K.IsSurfaceValid
• face_boundary_nonempty (f : K.Face) : 0 < K.faceBoundaryLength f

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.face_nonempty {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) : Nonempty K.Face

A polygonally valid complex has at least one face.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.inv_ne {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) (d : K.Dart) : K.inv d ≠ d

Inverse darts in a polygonally valid complex are distinct.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.interior_occurs_twice {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) (d : K.Dart) (hd : ¬K.IsBoundaryDart d) : K.OccursExactlyTwice d

A non-boundary edge in a valid incidence system occurs exactly twice.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.exists_unique_partner {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) (source : K.BoundaryOccurrence) (hsource : ¬K.IsBoundaryDart (K.occurrenceDart source)) : ∃! target : K.BoundaryOccurrence, source ≠ target ∧ (K.occurrenceDart target = K.occurrenceDart source ∨ K.occurrenceDart target = K.inv (K.occurrenceDart source))

Every internal occurrence has a unique distinct partner in its inverse-dart orbit.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.exists_pairing_source {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) (source : K.BoundaryOccurrence) (hsource : ¬K.IsBoundaryDart (K.occurrenceDart source)) : ∃ (pairing : K.BoundaryPairing), pairing.source = source

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

One-face presentation criterion

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.edgeName {Edge : Type} : SignedDart Edge → Edge

The unoriented edge name carried by a signed dart.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos e).edgeName = e
• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg e).edgeName = e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.edgeName_flip {Edge : Type} (d : SignedDart Edge) : d.flip.edgeName = d.edgeName

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.eq_or_eq_flip_iff_edgeName_eq {Edge : Type} (x d : SignedDart Edge) : x = d ∨ x = d.flip ↔ x.edgeName = d.edgeName

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.wordEdgeOccurrences {Edge : Type} [DecidableEq Edge] (word : List (SignedDart Edge)) (e : Edge) : Finset (Fin word.length)

Positions in a boundary word carrying either orientation of e.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.wordEdgeOccurrences word e = {i : Fin word.length | (word.get i).edgeName = e}

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.mem_wordEdgeOccurrences {Edge : Type} [DecidableEq Edge] (word : List (SignedDart Edge)) (e : Edge) (i : Fin word.length) : i ∈ wordEdgeOccurrences word e ↔ (word.get i).edgeName = e

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePresentation_isSurfaceValid {Edge : Type} [Fintype Edge] [DecidableEq Edge] (word : List (SignedDart Edge)) (hcard : ∀ (e : Edge), (wordEdgeOccurrences word e).card = 1 ∨ (wordEdgeOccurrences word e).card = 2) : (oneFacePresentation Edge word).IsSurfaceValid

A one-face presentation is incidence-valid when every edge name occurs once or twice, with orientation ignored. Boundary status is then derived from the occurrence count.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePresentation_occurrencePairingValid {Edge : Type} [Fintype Edge] [DecidableEq Edge] (word : List (SignedDart Edge)) (hword : word ≠ []) (hcard : ∀ (e : Edge), (wordEdgeOccurrences word e).card = 1 ∨ (wordEdgeOccurrences word e).card = 2) : (oneFacePresentation Edge word).OccurrencePairingValid

A nonempty, incidence-valid one-face word supplies polygonal pairing data.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.BoundaryPairing.identification {K : SurfaceCellComplex} (pairing : K.BoundaryPairing) : PolygonGluing.Identification K.Face K.faceBoundaryLength

The generic polygon-side identification associated to an occurrence pairing.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.polygonalIdentifications (K : SurfaceCellComplex) (_valid : K.OccurrencePairingValid) : Set (PolygonGluing.Identification K.Face K.faceBoundaryLength)

All side identifications compatible with a pairing-valid complex.

Equations

• K.polygonalIdentifications _valid = Set.range LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.BoundaryPairing.identification

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.pairing_identification_mem {K : SurfaceCellComplex} (valid : K.OccurrencePairingValid) (pairing : K.BoundaryPairing) : pairing.identification ∈ K.polygonalIdentifications valid

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.mem_polygonalIdentifications_iff_exists_occurrences {K : SurfaceCellComplex} (valid : K.OccurrencePairingValid) (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : identification ∈ K.polygonalIdentifications valid ↔ ∃ (source : K.BoundaryOccurrence) (target : K.BoundaryOccurrence), identification.source = K.occurrenceSide source ∧ identification.target = K.occurrenceSide target ∧ source ≠ target ∧ ¬K.IsBoundaryDart (K.occurrenceDart source) ∧ ¬K.IsBoundaryDart (K.occurrenceDart target) ∧ match identification.direction with | PolygonGluing.ParameterDirection.same => K.occurrenceDart target = K.occurrenceDart source | PolygonGluing.ParameterDirection.opposite => K.occurrenceDart target = K.inv (K.occurrenceDart source)

Membership in the polygonal identification set, unpacked into its two boundary occurrences.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFaceOccurrence {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) (i : Fin word.length) : (oneFacePresentation Edge word).BoundaryOccurrence

The boundary occurrence at position i in a one-face word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFaceOccurrence word i = ⟨PUnit.unit, i⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFaceOccurrence_dart {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) (i : Fin word.length) : (oneFacePresentation Edge word).occurrenceDart (oneFaceOccurrence word i) = word.get i

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFace_mem_polygonalIdentifications_iff {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) (valid : (oneFacePresentation Edge word).OccurrencePairingValid) (identification : PolygonGluing.Identification (oneFacePresentation Edge word).Face (oneFacePresentation Edge word).faceBoundaryLength) : identification ∈ (oneFacePresentation Edge word).polygonalIdentifications valid ↔ ∃ (i : Fin word.length) (j : Fin word.length), identification.source = (oneFacePresentation Edge word).occurrenceSide (oneFaceOccurrence word i) ∧ identification.target = (oneFacePresentation Edge word).occurrenceSide (oneFaceOccurrence word j) ∧ i ≠ j ∧ ¬(oneFacePresentation Edge word).IsBoundaryDart (word.get i) ∧ ¬(oneFacePresentation Edge word).IsBoundaryDart (word.get j) ∧ match identification.direction with | PolygonGluing.ParameterDirection.same => word.get j = word.get i | PolygonGluing.ParameterDirection.opposite => word.get j = (SignedDart.flipEquiv Edge) (word.get i)

For a one-face word, polygonal identifications are exactly compatible pairs of positions.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.not_isBoundaryDart_of_occurs_at_ne {K : SurfaceCellComplex} {d : K.Dart} {source target : K.BoundaryOccurrence} (hne : source ≠ target) (hsource : K.Occurs d source) (htarget : K.Occurs d target) : ¬K.IsBoundaryDart d

Two distinct occurrences of the same unoriented dart certify that it is internal.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification {K : SurfaceCellComplex} (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : PolygonGluing.Identification K.Face K.faceBoundaryLength

Reverse the directed presentation of a side identification.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification_source {K : SurfaceCellComplex} (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : (swapIdentification identification).source = identification.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification_target {K : SurfaceCellComplex} (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : (swapIdentification identification).target = identification.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification_direction {K : SurfaceCellComplex} (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : (swapIdentification identification).direction = identification.direction

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification_swap {K : SurfaceCellComplex} (identification : PolygonGluing.Identification K.Face K.faceBoundaryLength) : swapIdentification (swapIdentification identification) = identification

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.swapIdentification_mem_polygonalIdentifications {K : SurfaceCellComplex} (valid : K.OccurrencePairingValid) {identification : PolygonGluing.Identification K.Face K.faceBoundaryLength} (hidentification : identification ∈ K.polygonalIdentifications valid) : swapIdentification identification ∈ K.polygonalIdentifications valid

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oppositeDirectionIdentification_mem_of_get_pos_neg {Edge : Type} [Fintype Edge] (word : List (SignedDart Edge)) (valid : (oneFacePresentation Edge word).OccurrencePairingValid) (edge : Edge) (first second : Fin word.length) (hne : first ≠ second) (hfirst : word.get first = SignedDart.pos edge) (hsecond : word.get second = SignedDart.neg edge) : PolygonGluing.Identification.oppositeDirection ((oneFacePresentation Edge word).occurrenceSide (oneFaceOccurrence word first)) ((oneFacePresentation Edge word).occurrenceSide (oneFaceOccurrence word second)) ∈ (oneFacePresentation Edge word).polygonalIdentifications valid

A positive/negative pair of distinct word positions gives an opposite-direction identification.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccurrencePairingValid.exists_identification_source {K : SurfaceCellComplex} (h : K.OccurrencePairingValid) (source : K.BoundaryOccurrence) (hsource : ¬K.IsBoundaryDart (K.occurrenceDart source)) : ∃ identification ∈ K.polygonalIdentifications h, identification.source = K.occurrenceSide source

Under the occurrence-count conditions, every internal side starts an identification.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.PolygonalPreRealization (K : SurfaceCellComplex) : Type

The disjoint union of the polygonal cells indexed by the faces of K.

Equations

• K.PolygonalPreRealization = LeanEval.Topology.ClassificationOfSurfaces.PolygonGluing.PreRealization K.Face K.faceBoundaryLength

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.PolygonalGluingRel (K : SurfaceCellComplex) (valid : K.OccurrencePairingValid) : Setoid K.PolygonalPreRealization

The generated gluing relation associated to the boundary occurrences of pairing-valid K.

Equations

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

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.PolygonalRealization (K : SurfaceCellComplex) (valid : K.OccurrencePairingValid) : Type

The quotient of a pairing-valid complex by its compatible internal occurrence pairings.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.polygonalMk (K : SurfaceCellComplex) (valid : K.OccurrencePairingValid) : K.PolygonalPreRealization → K.PolygonalRealization valid

The quotient map from the polygonal disjoint union of K.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.continuous_polygonalMk (K : SurfaceCellComplex) (valid : K.OccurrencePairingValid) : Continuous (K.polygonalMk valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.isQuotientMap_polygonalMk (K : SurfaceCellComplex) (valid : K.OccurrencePairingValid) : Topology.IsQuotientMap (K.polygonalMk valid)

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

A compatible occurrence pairing identifies its side points in the polygonal quotient.

The two-monogon sphere presentation

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePositiveOccurrence : sphere.BoundaryOccurrence

The positively oriented side in the two-monogon sphere presentation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereNegativeOccurrence : sphere.BoundaryOccurrence

The negatively oriented side in the two-monogon sphere presentation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereNegativeOccurrence = ⟨true, ⟨0, LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereNegativeOccurrence._proof_1⟩⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.spherePositiveOccurrence_dart : sphere.occurrenceDart spherePositiveOccurrence = SignedDart.pos PUnit.unit

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereNegativeOccurrence_dart : sphere.occurrenceDart sphereNegativeOccurrence = SignedDart.neg PUnit.unit

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_inv_pos (e : PUnit.{1}) : sphere.inv (SignedDart.pos e) = SignedDart.neg e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_inv_neg (e : PUnit.{1}) : sphere.inv (SignedDart.neg e) = SignedDart.pos e

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_occurrencePairingValid : sphere.OccurrencePairingValid

The two-monogon sphere satisfies the occurrence-level pairing conditions.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_not_isBoundaryDart (d : sphere.Dart) : ¬sphere.IsBoundaryDart d

Neither oriented representative of the sphere edge is a boundary dart.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereBoundaryPairing : sphere.BoundaryPairing

The gluing from the positive monogon to the negative monogon.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphereBoundaryPairing_mem : sphereBoundaryPairing.identification ∈ sphere.polygonalIdentifications sphere_occurrencePairingValid