Finite surface cell complexes

This file owns the shared combinatorial API between the topological triangulation route and the Gallier-Xu normal-form route. The definitions are still intentionally light, but the public names and theorem boundaries match the Moise/PL blueprint.

structure LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex : Type 1

The raw finite incidence data underlying a Gallier-Xu surface cell complex.

Validity and connectedness are derived from this data by IsSurfaceValid and IsConnected, rather than stored as unconstrained propositions. Its faithful polygonal realization is constructed separately from the boundary occurrences.

• Face : Type

  The type of faces in the cell complex.

• Dart : Type

  The type of oriented darts in the cell complex.

• Vertex : Type

  The type of vertices in the cell complex.

• faceFintype : Fintype self.Face
• dartFintype : Fintype self.Dart
• vertexFintype : Fintype self.Vertex
• inv : self.Dart ≃ self.Dart

  Reversal of an oriented dart.

• source : self.Dart → self.Vertex

  The source vertex of an oriented dart.

• target : self.Dart → self.Vertex

  The target vertex of an oriented dart.

• boundary : self.Face → List self.Dart

  The cyclic boundary word of each face.

• inv_involutive (d : self.Dart) : self.inv (self.inv d) = d
• inv_source (d : self.Dart) : self.source (self.inv d) = self.target d
• inv_target (d : self.Dart) : self.target (self.inv d) = self.source d

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.numFaces (K : SurfaceCellComplex) : ℕ

The number of faces in a finite surface cell complex.

Equations

• K.numFaces = Fintype.card K.Face

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.numDarts (K : SurfaceCellComplex) : ℕ

The number of oriented darts in a finite surface cell complex.

Equations

• K.numDarts = Fintype.card K.Dart

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.numVertices (K : SurfaceCellComplex) : ℕ

The number of vertices in a finite surface cell complex.

Equations

• K.numVertices = Fintype.card K.Vertex

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.faceBoundaryLength (K : SurfaceCellComplex) (f : K.Face) : ℕ

The length of a face boundary word.

Equations

• K.faceBoundaryLength f = (K.boundary f).length

@[reducible, inline]

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

A position in one of the stored, positively oriented face boundaries.

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.boundaryOccurrenceFintype (K : SurfaceCellComplex) : Fintype K.BoundaryOccurrence

Equations

• K.boundaryOccurrenceFintype = inferInstance

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.BoundaryOccurrence.dart {K : SurfaceCellComplex} (o : K.BoundaryOccurrence) : K.Dart

The dart stored at a boundary occurrence.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SameEdge (K : SurfaceCellComplex) (d e : K.Dart) : Prop

Two darts name the same unoriented edge.

Equations

• K.SameEdge d e = (e = d ∨ e = K.inv d)

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.Occurs (K : SurfaceCellComplex) (d : K.Dart) (o : K.BoundaryOccurrence) : Prop

A boundary position belongs to the unoriented edge named by d.

Equations

• K.Occurs d o = K.SameEdge d o.dart

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccursExactlyOnce (K : SurfaceCellComplex) (d : K.Dart) : Prop

The unoriented edge named by d occurs at exactly one boundary position.

Equations

• K.OccursExactlyOnce d = ∃ (o : K.BoundaryOccurrence), K.Occurs d o ∧ ∀ (o' : K.BoundaryOccurrence), K.Occurs d o' → o' = o

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.OccursExactlyTwice (K : SurfaceCellComplex) (d : K.Dart) : Prop

The unoriented edge named by d occurs at exactly two boundary positions.

Equations

• K.OccursExactlyTwice d = ∃ (o₁ : K.BoundaryOccurrence) (o₂ : K.BoundaryOccurrence), o₁ ≠ o₂ ∧ K.Occurs d o₁ ∧ K.Occurs d o₂ ∧ ∀ (o : K.BoundaryOccurrence), K.Occurs d o → o = o₁ ∨ o = o₂

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.IsBoundaryDart (K : SurfaceCellComplex) (d : K.Dart) : Prop

Boundary status derived from incidence: the edge orbit of d occurs exactly once.

Equations

• K.IsBoundaryDart d = K.OccursExactlyOnce d

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.IsSurfaceValid (K : SurfaceCellComplex) : Prop

Incidence validity for the stored face-boundary system.

There is at least one face, different faces have different cyclic boundary words, inverse darts are distinct, and every unoriented edge occurs either once (a boundary edge) or twice (an inner edge). Boundary status and occurrence counts are derived from explicit boundary positions, so repeated darts such as the projective-plane word a a are retained. The stored vertex endpoints are an enrichment of Gallier--Xu's boundary-word data and are deliberately not part of this predicate.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sameEdge_inv_left_iff (K : SurfaceCellComplex) (d e : K.Dart) : K.SameEdge (K.inv d) e ↔ K.SameEdge d e

Inverting the chosen representative does not change its unoriented edge.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.occurs_inv_iff (K : SurfaceCellComplex) (d : K.Dart) (o : K.BoundaryOccurrence) : K.Occurs (K.inv d) o ↔ K.Occurs d o

Inverting the chosen representative does not change which boundary positions it occupies.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.isBoundaryDart_inv_iff (K : SurfaceCellComplex) (d : K.Dart) : K.IsBoundaryDart (K.inv d) ↔ K.IsBoundaryDart d

Boundary status is invariant under reversing the representative dart.

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

Inverse darts in a valid incidence system are distinct.

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

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.FaceAdjacent (K : SurfaceCellComplex) (f g : K.Face) : Prop

Two faces are adjacent when their boundaries use the same unoriented edge.

Equations

• K.FaceAdjacent f g = ∃ d ∈ K.boundary f, ∃ e ∈ K.boundary g, K.SameEdge d e

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.IsConnected (K : SurfaceCellComplex) : Prop

Gallier-Xu connectivity of the face-edge incidence system.

Equations

• K.IsConnected = (Nonempty K.Face ∧ ∀ (f g : K.Face), Relation.ReflTransGen K.FaceAdjacent f g)

inductive LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart (α : Type u_1) : Type u_1

A signed occurrence of a named edge in a polygonal boundary word.

• pos {α : Type u_1} : α → SignedDart α
• neg {α : Type u_1} : α → SignedDart α

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instDecidableEqSignedDart.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : SignedDart α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instDecidableEqSignedDart {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (SignedDart α✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instDecidableEqSignedDart = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instDecidableEqSignedDart.decEq

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instReprSignedDart {α✝ : Type u_1} [Repr α✝] : Repr (SignedDart α✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instReprSignedDart = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instReprSignedDart.repr }

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instReprSignedDart.repr {α✝ : Type u_1} [Repr α✝] : SignedDart α✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.instFintypeSignedDart {α✝ : Type u_1} [Fintype α✝] : Fintype (SignedDart α✝)

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.edge {α : Type u_1} : SignedDart α → α

The underlying unoriented edge name of a signed dart.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos a).edge = a
• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg a).edge = a

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.flip {α : Type u_1} : SignedDart α → SignedDart α

Reverse the orientation of a signed dart.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos a).flip = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg a
• (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg a).flip = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.edge_flip {α : Type u_1} (d : SignedDart α) : d.flip.edge = d.edge

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.flip_flip {α : Type u_1} (d : SignedDart α) : d.flip.flip = d

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.flipEquiv (α : Type u_1) : SignedDart α ≃ SignedDart α

Orientation reversal as an equivalence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.flipEquiv_apply {α : Type u_1} (d : SignedDart α) : (flipEquiv α) d = d.flip

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePresentation (Edge : Type) [Fintype Edge] (word : List (SignedDart Edge)) : SurfaceCellComplex

A single-face polygonal presentation with all edge names based at one vertex.

This constructor is intentionally simple. It is useful for normal-form examples and for the Gallier-Xu boundary-word API.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePresentation_isConnected (Edge : Type) [Fintype Edge] (word : List (SignedDart Edge)) : (oneFacePresentation Edge word).IsConnected

Every one-face presentation is connected in the face-edge incidence sense.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartOfOrientedEdge {Edge : Type u_1} : OrientedEdge Edge → SignedDart Edge

Convert an oriented triangulation edge occurrence to a cell-complex signed dart.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartOfOrientedEdge_injective {Edge : Type u_1} : Function.Injective signedDartOfOrientedEdge

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartOfOrientedEdge_edge {Edge : Type u_1} (d : OrientedEdge Edge) : (signedDartOfOrientedEdge d).edge = d.edge

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

The sphere presented as two monogons with oppositely oriented copies of one edge.

The nonempty boundary presentation is equivalent to Gallier--Xu's empty-word sphere and is directly compatible with the polygonal occurrence adapter.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_isSurfaceValid : sphere.IsSurfaceValid

The two-monogon presentation of the sphere has valid incidence data.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere_isConnected : sphere.IsConnected

The two faces of the sphere presentation are connected through their common edge.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toCellComplex {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : SurfaceCellComplex

Raw compatibility bridge from the ledgered triangulation record to stored cell-presentation data.

This conversion does not prove IsSurfaceValid or IsConnected; in particular, those properties do not follow from FiniteSurfaceTriangulation.Valid. New geometric work should start from GeometricTriangulation, and downstream cellulation work must separately certify the incidence predicates.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toCellComplex_sameEdge_iff {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (d e : T.toCellComplex.Dart) : T.toCellComplex.SameEdge d e ↔ SurfaceCellComplex.SignedDart.edge e = SurfaceCellComplex.SignedDart.edge d

def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : T.BoundaryPosition ≃ T.toCellComplex.BoundaryOccurrence

Triangle-boundary positions are canonically the boundary occurrences of the converted cell complex.

Equations

• T.boundaryPositionEquivCellOccurrence = Equiv.sigmaCongrRight fun (x : T.Triangle) => (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence_apply_fst {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.BoundaryPosition) : (T.boundaryPositionEquivCellOccurrence o).fst = o.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence_apply_val {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.BoundaryPosition) : ↑(T.boundaryPositionEquivCellOccurrence o).snd = ↑o.snd

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence_symm_apply_fst {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.toCellComplex.BoundaryOccurrence) : (T.boundaryPositionEquivCellOccurrence.symm o).fst = o.fst

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence_symm_apply_val {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.toCellComplex.BoundaryOccurrence) : ↑(T.boundaryPositionEquivCellOccurrence.symm o).snd = ↑o.snd

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryPositionEquivCellOccurrence_dart {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.BoundaryPosition) : (T.boundaryPositionEquivCellOccurrence o).dart = SurfaceCellComplex.signedDartOfOrientedEdge o.orientedEdge

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.sameEdge_boundaryPositionEquivCellOccurrence_iff {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (d : T.toCellComplex.Dart) (o : T.BoundaryPosition) : T.toCellComplex.SameEdge d (T.boundaryPositionEquivCellOccurrence o).dart ↔ o.edge = SurfaceCellComplex.SignedDart.edge d

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toCellComplex_isSurfaceValid_of_incidenceCertificate {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (h : T.IncidenceCertificate) : T.toCellComplex.IsSurfaceValid

An incidence-certified finite triangulation produces valid cell-complex incidence data.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toCellComplex_isConnected_of_incidenceCertificate {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (h : T.IncidenceCertificate) : T.toCellComplex.IsConnected

Dual connectivity of a certified triangulation gives cell-complex face connectivity.