Finite signed-dart presentations

This file removes arbitrary dart names from a finite surface cell complex. Unoriented edges are the quotient of darts by orientation reversal. When reversal has no fixed points, choosing one orientation in each orbit identifies all darts with signed orbit names, and a final finite relabeling gives names in Fin.

The construction uses only Dart, inv, finiteness, and the involution laws. In particular it does not trust the stored vertex endpoints. This is the combinatorial input needed before cyclic boundary-word moves can be stated independently of a presentation's original edge names.

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.mapEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) : SignedDart α ≃ SignedDart β

Relabel signed darts along an equivalence of edge names.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.mapEquiv_pos {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : α) : (mapEquiv e) (pos a) = pos (e a)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.mapEquiv_neg {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : α) : (mapEquiv e) (neg a) = neg (e a)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.mapEquiv_flip {α : Type u_1} {β : Type u_2} (e : α ≃ β) (d : SignedDart α) : (mapEquiv e) d.flip = ((mapEquiv e) d).flip

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.edgeSetoid (K : SurfaceCellComplex) : Setoid K.Dart

The equivalence relation on darts generated by reversing orientation.

Equations

• K.edgeSetoid = { r := K.SameEdge, iseqv := ⋯ }

@[reducible, inline]

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

Unoriented edges are inverse-dart orbits.

Equations

• K.EdgeOrbit = Quotient K.edgeSetoid

def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.edgeOrbit (K : SurfaceCellComplex) (d : K.Dart) : K.EdgeOrbit

The unoriented edge containing a dart.

Equations

• K.edgeOrbit d = ⟦d⟧

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.edgeOrbit_eq_iff (K : SurfaceCellComplex) (d e : K.Dart) : K.edgeOrbit d = K.edgeOrbit e ↔ K.SameEdge d e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.edgeOrbit_inv (K : SurfaceCellComplex) (d : K.Dart) : K.edgeOrbit (K.inv d) = K.edgeOrbit d

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.edgeOrbitFintype (K : SurfaceCellComplex) : Fintype K.EdgeOrbit

Equations

• K.edgeOrbitFintype = Fintype.ofFinite K.EdgeOrbit

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartEquiv (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) : SignedDart K.EdgeOrbit ≃ K.Dart

A fixed-point-free involution presents the darts as signed unoriented edges.

Equations

• K.signedDartEquiv hinv = Equiv.ofBijective (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartToDart✝ K) ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.signedDartEquiv_symm_inv (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) (d : K.Dart) : (K.signedDartEquiv hinv).symm (K.inv d) = ((K.signedDartEquiv hinv).symm d).flip

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.numEdgeOrbits (K : SurfaceCellComplex) : ℕ

The number of unoriented edges, computed as the number of inverse-dart orbits.

Equations

• K.numEdgeOrbits = Fintype.card K.EdgeOrbit

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.finSignedDartEquiv (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) : K.Dart ≃ SignedDart (Fin K.numEdgeOrbits)

Relabel arbitrary darts as signed Fin-labelled unoriented edges.

Equations

• K.finSignedDartEquiv hinv = (K.signedDartEquiv hinv).symm.trans (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.mapEquiv (Fintype.equivFin K.EdgeOrbit))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.finSignedDartEquiv_inv (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) (d : K.Dart) : (K.finSignedDartEquiv hinv) (K.inv d) = ((K.finSignedDartEquiv hinv) d).flip

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.normalizedBoundary (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) (f : K.Face) : List (SignedDart (Fin K.numEdgeOrbits))

A face boundary with its arbitrary dart names replaced by signed finite edge labels.

Equations

• K.normalizedBoundary hinv f = List.map (⇑(K.finSignedDartEquiv hinv)) (K.boundary f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.normalizedBoundary_length (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) (f : K.Face) : (K.normalizedBoundary hinv f).length = K.faceBoundaryLength f

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.normalizedBoundary_map_symm (K : SurfaceCellComplex) (hinv : ∀ (d : K.Dart), K.inv d ≠ d) (f : K.Face) : List.map (⇑(K.finSignedDartEquiv hinv).symm) (K.normalizedBoundary hinv f) = K.boundary f

Finite relabeling loses no information from a face boundary.