Finite cyclic presentations of triangulations

This file relabels the finite faces and unoriented edges of a surface triangulation by Fin. Each oriented triangle boundary is transported to a cyclic word of signed finite edge names. Incidence validity and dual connectivity then pass to the resulting FiniteCyclicPresentation.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicDartEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : OrientedEdge T.Edge ≃ SurfaceCellComplex.SignedDart (Fin (Fintype.card T.Edge))

Relabel an oriented triangulation edge by a signed Fin edge name.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.edgeOfDart_finiteCyclicDartEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (d : OrientedEdge T.Edge) : FiniteCyclicPresentation.edgeOfDart (T.finiteCyclicDartEquiv d) = (Fintype.equivFin T.Edge) d.edge

@[reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : FiniteCyclicPresentation

Enumerate the faces and unoriented edges of a finite triangulation and retain its cyclic signed triangle boundaries.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_faces_length {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : T.toFiniteCyclicPresentation.faces.length = Fintype.card T.Triangle

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicEdgeEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : T.Edge ≃ T.toFiniteCyclicPresentation.Edge

The original unoriented edge names are equivalent to the enumerated presentation edges.

Equations

• T.finiteCyclicEdgeEquiv = id (Fintype.equivFin T.Edge)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.edgeOfDart_finiteCyclicDartEquiv_eq_edgeEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (d : OrientedEdge T.Edge) : FiniteCyclicPresentation.edgeOfDart (T.finiteCyclicDartEquiv d) = T.finiteCyclicEdgeEquiv d.edge

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicFaceEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : T.Triangle ≃ T.toFiniteCyclicPresentation.Face

The original triangles are equivalent to positions in the presentation's face list.

Equations

• T.finiteCyclicFaceEquiv = (Fintype.equivFin T.Triangle).trans (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicFaceEquiv_apply_val {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) : ↑(T.finiteCyclicFaceEquiv f) = ↑((Fintype.equivFin T.Triangle) f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicFaceEquiv_symm_apply_val {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.toFiniteCyclicPresentation.Face) : ↑((Fintype.equivFin T.Triangle) (T.finiteCyclicFaceEquiv.symm f)) = ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_boundary_faceEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) : T.toFiniteCyclicPresentation.boundary (T.finiteCyclicFaceEquiv f) = List.map (⇑T.finiteCyclicDartEquiv) (T.triangleBoundary f)

Reading an enumerated face gives exactly the relabeled original triangle boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_boundary_faceEquiv_length {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) : (T.toFiniteCyclicPresentation.boundary (T.finiteCyclicFaceEquiv f)).length = (T.triangleBoundary f).length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_boundary_faceEquiv_get {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) (i : Fin (T.toFiniteCyclicPresentation.boundary (T.finiteCyclicFaceEquiv f)).length) : (T.toFiniteCyclicPresentation.boundary (T.finiteCyclicFaceEquiv f)).get i = T.finiteCyclicDartEquiv ((T.triangleBoundary f).get (Fin.cast ⋯ i))

Reading a position in an enumerated boundary is the same as reading the corresponding position before relabeling and then relabeling its dart.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicOccurrenceEquiv {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) : T.BoundaryPosition ≃ (f : T.toFiniteCyclicPresentation.Face) × Fin (T.toFiniteCyclicPresentation.boundary f).length

Original triangle-boundary positions are canonically the boundary occurrences of the enumerated cyclic presentation.

Equations

• T.finiteCyclicOccurrenceEquiv = T.finiteCyclicFaceEquiv.sigmaCongr fun (f : T.Triangle) => (Fin.castOrderIso ⋯).toEquiv

@[simp]

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

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.finiteCyclicOccurrenceEquiv_dart {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (o : T.BoundaryPosition) : (T.toFiniteCyclicPresentation.boundary (T.finiteCyclicOccurrenceEquiv o).fst).get (T.finiteCyclicOccurrenceEquiv o).snd = T.finiteCyclicDartEquiv o.orientedEdge

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.boundaryEdgeCount {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) (e : T.Edge) : ℕ

Number of occurrences of an original unoriented edge in one stored triangle boundary.

Equations

• T.boundaryEdgeCount f e = List.count e (List.map LeanEval.Topology.ClassificationOfSurfaces.OrientedEdge.edge (T.triangleBoundary f))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.edgeOccurrenceCount {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (e : T.Edge) : ℕ

Total number of boundary positions occupied by an original unoriented edge.

Equations

• T.edgeOccurrenceCount e = {o : T.BoundaryPosition | o.edge = e}.card

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_faceEdgeMultiplicity {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (f : T.Triangle) (e : T.Edge) : T.toFiniteCyclicPresentation.faceEdgeMultiplicity (T.finiteCyclicFaceEquiv f) (T.finiteCyclicEdgeEquiv e) = T.boundaryEdgeCount f e

Relabeling a face and an edge does not change the number of times that edge occurs in the face boundary.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_edgeMultiplicity {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (e : T.Edge) : T.toFiniteCyclicPresentation.edgeMultiplicity (T.finiteCyclicEdgeEquiv e) = T.edgeOccurrenceCount e

The total multiplicity of an enumerated edge is the cardinality of its original boundary position fiber.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteSurfaceTriangulation.toFiniteCyclicPresentation_isSurfaceValid {S : Type u_1} [TopologicalSpace S] (T : FiniteSurfaceTriangulation S) (h : T.IncidenceCertificate) (hboundary : ∀ (f : T.Triangle), T.triangleBoundary f ≠ []) : T.toFiniteCyclicPresentation.IsSurfaceValid

An incidence certificate and nonempty stored face boundaries give a valid finite cyclic presentation. The boundary hypothesis is separate because the legacy certificate permits an otherwise vacuous empty boundary.

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

A dual-connected incidence certificate gives connectivity of the enumerated finite cyclic presentation.

@[reducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteCyclicPresentation {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : FiniteCyclicPresentation

The finite cyclic presentation underlying a geometric triangulation.

Equations

• T.toFiniteCyclicPresentation = T.toFiniteSurfaceTriangulation.toFiniteCyclicPresentation

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteCyclicPresentation_isSurfaceValid {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (h : T.SurfaceIncidence) : T.toFiniteCyclicPresentation.IsSurfaceValid

Surface incidence makes the cyclic presentation of a geometric triangulation valid.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteCyclicPresentation_isConnected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (h : T.SurfaceIncidence) : T.toFiniteCyclicPresentation.IsConnected

Surface incidence makes the cyclic presentation of a geometric triangulation connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.toFiniteCyclicPresentation_valid_and_connected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (h : T.SurfaceIncidence) : T.toFiniteCyclicPresentation.IsSurfaceValid ∧ T.toFiniteCyclicPresentation.IsConnected

A geometric surface triangulation therefore supplies the valid, connected finite signed cyclic presentation needed by the normal-form lane.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.compactEvalSurfaceFiniteCyclicPresentation (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : FiniteCyclicPresentation

The named finite cyclic presentation obtained by enumerating the Radó triangulation of a compact connected Eval surface.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_finiteCyclicPresentation_isSurfaceValid (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : (compactEvalSurfaceFiniteCyclicPresentation S).IsSurfaceValid

The finite cyclic presentation attached to a compact connected Eval surface is valid.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_finiteCyclicPresentation_isConnected (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : (compactEvalSurfaceFiniteCyclicPresentation S).IsConnected

The finite cyclic presentation attached to a compact connected Eval surface is connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_has_valid_connected_finiteCyclicPresentation (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : ∃ (P : FiniteCyclicPresentation), P.IsSurfaceValid ∧ P.IsConnected

The Eval hypotheses therefore supply a valid, connected finite cyclic presentation, which is the input expected by the Gallier--Xu normal-form lane.