Faithful polygonal realization of a geometric triangulation

The local map in this file identifies each three-sided polygon cell with the corresponding barycentric face. Its side formula uses the cyclic face order exactly, so adjacent face maps agree under the signed occurrence pairing.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceCellHomeomorph {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.Triangle) : PolygonCell 3 ≃ₜ T.toIntrinsic.ClosedFace f

A three-sided polygon cell is canonically identified with one closed barycentric face.

Equations

• T.faceCellHomeomorph f = LeanEval.Topology.ClassificationOfSurfaces.TriangleCell.cellHomeomorph.trans (T.toIntrinsic.facePlaneHomeomorph f).symm

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceVertexEmbedding_eq_cyclic {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.Triangle) (i : Fin 3) : (T.toIntrinsic.faceVertexEmbedding f) i = T.toIntrinsic.faceVertex f ((ZMod.finEquiv 3) i)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceCellHomeomorph_side {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.Triangle) (i : Fin 3) (r : ↑unitInterval) : ↑↑((T.faceCellHomeomorph f) ((PolygonCell.side i) r)) = (AffineMap.lineMap (Pi.single ((T.toIntrinsic.faceVertexEmbedding f) i) 1) (Pi.single ((T.toIntrinsic.faceVertexEmbedding f) ((finRotate 3) i)) 1)) ↑r

On cyclic side i, the face-cell map is the affine barycentric path from face vertex i to face vertex i+1.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicFace {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) : T.Triangle

Recover the geometric triangle represented by an enumerated cyclic face.

Equations

• T.cyclicFace f = T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv.symm f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicFace_finiteCyclicFaceEquiv {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.Triangle) : T.cyclicFace (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv f) = f

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.finiteCyclicFaceEquiv_cyclicFace {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) : T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv (T.cyclicFace f) = f

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicBoundaryLength {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) : (T.toFiniteCyclicPresentation.boundary f).length = 3

Every polygon appearing in the cyclic presentation of a triangulation has three marked sides.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonFaceHomeomorph {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) : PolygonCell (T.toFiniteCyclicPresentation.boundary f).length ≃ₜ T.toIntrinsic.ClosedFace (T.cyclicFace f)

The enumerated polygon for f, including its stored side-count type, is homeomorphic to the corresponding closed geometric face.

Equations

• T.polygonFaceHomeomorph f = (LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.castHomeomorph ⋯).trans (T.faceCellHomeomorph (T.cyclicFace f))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalPreMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : T.toFiniteCyclicPresentation.PolygonalPreRealization → ↑T.realization

The facewise map on the disjoint union of cyclic polygon cells.

Equations

• T.polygonalPreMap x = ↑((T.polygonFaceHomeomorph x.fst) x.snd)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.continuous_polygonalPreMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Continuous T.polygonalPreMap

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicOrientedEdge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (o : T.toFiniteCyclicPresentation.BoundaryOccurrence) : OrientedEdge T.Edge

The original oriented geometric edge stored at an enumerated boundary occurrence.

Equations

• T.cyclicOrientedEdge o = T.orientedFaceEdge (T.cyclicFace o.fst) ((ZMod.finEquiv 3) (Fin.cast ⋯ o.snd))

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicOccurrence {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) (i : Fin 3) : T.toFiniteCyclicPresentation.BoundaryOccurrence

The boundary occurrence belonging to a specified Fin 3 side of an enumerated face.

Equations

• T.cyclicOccurrence f i = ⟨f, Fin.cast ⋯ i⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicOccurrence_face {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) (i : Fin 3) : (T.cyclicOccurrence f i).fst = f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicOccurrence_index_cast {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) (i : Fin 3) : Fin.cast ⋯ (T.cyclicOccurrence f i).snd = i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.cyclicOrientedEdge_cyclicOccurrence {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) (i : Fin 3) : T.cyclicOrientedEdge (T.cyclicOccurrence f i) = T.orientedFaceEdge (T.cyclicFace f) ((ZMod.finEquiv 3) i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.finiteCyclicDartEquiv_cyclicOrientedEdge {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (o : T.toFiniteCyclicPresentation.BoundaryOccurrence) : T.toFiniteSurfaceTriangulation.finiteCyclicDartEquiv (T.cyclicOrientedEdge o) = o.dart

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.finiteCyclicDartEquiv_flip {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (d : OrientedEdge T.Edge) : T.toFiniteSurfaceTriangulation.finiteCyclicDartEquiv d.flip = (T.toFiniteSurfaceTriangulation.finiteCyclicDartEquiv d).flip

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedEdgeSource_flip {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (d : OrientedEdge T.Edge) : T.orientedEdgeSource d.flip = T.orientedEdgeTarget d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.orientedEdgeTarget_flip {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (d : OrientedEdge T.Edge) : T.orientedEdgeTarget d.flip = T.orientedEdgeSource d

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonFaceHomeomorph_side {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (f : T.toFiniteCyclicPresentation.Face) (i : Fin (T.toFiniteCyclicPresentation.boundary f).length) (r : ↑unitInterval) : ↑↑((T.polygonFaceHomeomorph f) ((PolygonCell.side i) r)) = (AffineMap.lineMap (Pi.single ((T.toIntrinsic.faceVertexEmbedding (T.cyclicFace f)) (Fin.cast ⋯ i)) 1) (Pi.single ((T.toIntrinsic.faceVertexEmbedding (T.cyclicFace f)) ((finRotate 3) (Fin.cast ⋯ i))) 1)) ↑r

The enumerated side parameter is carried to the corresponding affine edge parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonFaceHomeomorph_side_oriented {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (o : T.toFiniteCyclicPresentation.BoundaryOccurrence) (r : ↑unitInterval) : ↑↑((T.polygonFaceHomeomorph o.fst) ((PolygonCell.side o.snd) r)) = (AffineMap.lineMap (Pi.single (T.orientedEdgeSource (T.cyclicOrientedEdge o)) 1) (Pi.single (T.orientedEdgeTarget (T.cyclicOrientedEdge o)) 1)) ↑r

The affine endpoints of an enumerated side are the source and target of its original oriented geometric edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.exists_orientedEdgeParameter {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (d : OrientedEdge T.Edge) (x : ↑T.realization) (hx : x ∈ T.toIntrinsic.faceCarrier ↑d.edge) : ∃ (r : ↑unitInterval), ↑x = (AffineMap.lineMap (Pi.single (T.orientedEdgeSource d) 1) (Pi.single (T.orientedEdgeTarget d) 1)) ↑r

Every point of a geometric edge has the affine parameterization determined by either orientation of that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalPreMap_pairing_eq {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (pairing : T.toFiniteCyclicPresentation.BoundaryPairing) (r : ↑unitInterval) : T.polygonalPreMap (pairing.identification.source.point r) = T.polygonalPreMap (pairing.identification.target.point (pairing.identification.parameter r))

Compatible signed occurrence pairings have identical images under the facewise geometric map.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalPreMap_respects {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) {x y : T.toFiniteCyclicPresentation.PolygonalPreRealization} (hxy : (T.toFiniteCyclicPresentation.PolygonalGluingRel valid) x y) : T.polygonalPreMap x = T.polygonalPreMap y

The facewise map is constant on the equivalence relation generated by all compatible pairings.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealizationMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) : T.toFiniteCyclicPresentation.PolygonalRealization valid → ↑T.realization

Descend the calibrated face maps through the cyclic polygonal quotient.

Equations

• T.polygonalRealizationMap valid = Quotient.lift T.polygonalPreMap ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealizationMap_mk {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (x : T.toFiniteCyclicPresentation.PolygonalPreRealization) : T.polygonalRealizationMap valid (T.toFiniteCyclicPresentation.polygonalMk valid x) = T.polygonalPreMap x

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.continuous_polygonalRealizationMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) : Continuous (T.polygonalRealizationMap valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.surjective_polygonalPreMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) : Function.Surjective T.polygonalPreMap

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.surjective_polygonalRealizationMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) : Function.Surjective (T.polygonalRealizationMap valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalMk_side_eq_of_orientedEdge_eq {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) {o p : T.toFiniteCyclicPresentation.BoundaryOccurrence} (hop : o ≠ p) (hedge : T.cyclicOrientedEdge p = T.cyclicOrientedEdge o) (r : ↑unitInterval) : T.toFiniteCyclicPresentation.polygonalMk valid ((T.toFiniteCyclicPresentation.occurrenceSide o).point r) = T.toFiniteCyclicPresentation.polygonalMk valid ((T.toFiniteCyclicPresentation.occurrenceSide p).point r)

Two distinct occurrences carrying the same oriented geometric edge identify equal side parameters in the polygonal quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalMk_side_eq_of_orientedEdge_eq_flip {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) {o p : T.toFiniteCyclicPresentation.BoundaryOccurrence} (hop : o ≠ p) (hedge : T.cyclicOrientedEdge p = (T.cyclicOrientedEdge o).flip) (r : ↑unitInterval) : T.toFiniteCyclicPresentation.polygonalMk valid ((T.toFiniteCyclicPresentation.occurrenceSide o).point r) = T.toFiniteCyclicPresentation.polygonalMk valid ((T.toFiniteCyclicPresentation.occurrenceSide p).point (unitInterval.symm r))

Two distinct occurrences carrying oppositely oriented copies of one geometric edge identify opposite side parameters in the polygonal quotient.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (f : T.toFiniteCyclicPresentation.Face) : T.toIntrinsic.ClosedFace (T.cyclicFace f) → T.toFiniteCyclicPresentation.PolygonalRealization valid

Invert one calibrated face map and include that polygon in the quotient.

Equations

• T.faceQuotientMap valid f x = T.toFiniteCyclicPresentation.polygonalMk valid ⟨f, (T.polygonFaceHomeomorph f).symm x⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.closedFaceCastHomeomorph {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) {f g : T.Triangle} (h : f = g) : T.toIntrinsic.ClosedFace f ≃ₜ T.toIntrinsic.ClosedFace g

Transport a closed face along equality of its face name.

Equations

• T.closedFaceCastHomeomorph h = h ▸ Homeomorph.refl (T.toIntrinsic.ClosedFace f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.closedFaceCastHomeomorph_val {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) {f g : T.Triangle} (h : f = g) (x : T.toIntrinsic.ClosedFace f) : ↑((T.closedFaceCastHomeomorph h) x) = ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.continuous_faceQuotientMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (f : T.toFiniteCyclicPresentation.Face) : Continuous (T.faceQuotientMap valid f)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_congr {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) {f g : T.toFiniteCyclicPresentation.Face} (hfg : f = g) (x : T.toIntrinsic.ClosedFace (T.cyclicFace f)) (y : T.toIntrinsic.ClosedFace (T.cyclicFace g)) (hxy : ↑x = ↑y) : T.faceQuotientMap valid f x = T.faceQuotientMap valid g y

Changing only the proof-level name of a packed face does not change its inverse quotient value.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_faceHomeomorph {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (f : T.toFiniteCyclicPresentation.Face) (z : PolygonCell (T.toFiniteCyclicPresentation.boundary f).length) : T.faceQuotientMap valid f ((T.polygonFaceHomeomorph f) z) = T.toFiniteCyclicPresentation.polygonalMk valid ⟨f, z⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_eq_of_inter_card_two {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) {f g : T.toFiniteCyclicPresentation.Face} (hfg : f ≠ g) (hcard : (↑(T.cyclicFace f) ∩ ↑(T.cyclicFace g)).card = 2) (x : ↑T.realization) (hxf : x ∈ T.toIntrinsic.faceCarrier ↑(T.cyclicFace f)) (hxg : x ∈ T.toIntrinsic.faceCarrier ↑(T.cyclicFace g)) : T.faceQuotientMap valid f ⟨x, hxf⟩ = T.faceQuotientMap valid g ⟨x, hxg⟩

The two inverse face maps agree in the quotient along a common geometric edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_eq_vertexPoint_of_faceAdjacentAtVertex {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (v : T.toIntrinsic.UsedVertex) {f g : T.Triangle} (hvf : ↑v ∈ ↑f) (hvg : ↑v ∈ ↑g) (hadj : TriangleFamily.FaceAdjacentAtVertex T.faces (↑v) f g) : T.faceQuotientMap valid (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv f) ⟨T.toIntrinsic.vertexPoint v, ⋯⟩ = T.faceQuotientMap valid (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv g) ⟨T.toIntrinsic.vertexPoint v, ⋯⟩

At a fixed vertex, inverse face maps agree across one star-adjacency step.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_eq_vertexPoint {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) (v : T.toIntrinsic.UsedVertex) (f g : T.Triangle) (hvf : ↑v ∈ ↑f) (hvg : ↑v ∈ ↑g) : T.faceQuotientMap valid (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv f) ⟨T.toIntrinsic.vertexPoint v, ⋯⟩ = T.faceQuotientMap valid (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv g) ⟨T.toIntrinsic.vertexPoint v, ⋯⟩

Strong fixed-star connectivity makes the quotient value of a vertex independent of the incident face used to compute it.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faceQuotientMap_eq_of_mem {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) (f g : T.toFiniteCyclicPresentation.Face) (x : ↑T.realization) (hxf : x ∈ T.toIntrinsic.faceCarrier ↑(T.cyclicFace f)) (hxg : x ∈ T.toIntrinsic.faceCarrier ↑(T.cyclicFace g)) : T.faceQuotientMap valid f ⟨x, hxf⟩ = T.faceQuotientMap valid g ⟨x, hxg⟩

Under strong fixed-star connectivity, inverse face maps agree on every face overlap.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.realizationInverse {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (x : ↑T.realization) : T.toFiniteCyclicPresentation.PolygonalRealization valid

Choose one containing face and use its inverse face map. Overlap compatibility makes this choice immaterial.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.realizationInverse_eqOn_face {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) (f : T.Triangle) (x : ↑T.realization) (hxf : x ∈ T.toIntrinsic.faceCarrier ↑f) : T.realizationInverse valid x = T.faceQuotientMap valid (T.toFiniteSurfaceTriangulation.finiteCyclicFaceEquiv f) ⟨x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.continuous_realizationInverse {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) : Continuous (T.realizationInverse valid)

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealizationMap_realizationInverse {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (x : ↑T.realization) : T.polygonalRealizationMap valid (T.realizationInverse valid x) = x

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.realizationInverse_polygonalRealizationMap {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) (q : T.toFiniteCyclicPresentation.PolygonalRealization valid) : T.realizationInverse valid (T.polygonalRealizationMap valid q) = q

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealizationHomeomorph {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) : T.toFiniteCyclicPresentation.PolygonalRealization valid ≃ₜ ↑T.realization

The faithful homeomorphism from the cyclic polygonal quotient to the barycentric geometric realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealization_homeomorphic {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) (hstar : TriangleFamily.IsStrongVertexStarConnected T.faces) : Nonempty (T.toFiniteCyclicPresentation.PolygonalRealization valid ≃ₜ ↑T.realization)

Existence form used by the classification pipeline.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.polygonalRealization_homeomorphic_of_surface {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] (valid : T.toFiniteCyclicPresentation.IsSurfaceValid) : Nonempty (T.toFiniteCyclicPresentation.PolygonalRealization valid ≃ₜ ↑T.realization)

For a genuine surface triangulation, fixed-star connectivity follows from the manifold charts, so the faithful polygonal realization needs no extra combinatorial hypothesis.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_geometricTriangulation_isStrongVertexStarConnected (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : TriangleFamily.IsStrongVertexStarConnected (compactEvalSurfaceGeometricTriangulation S).faces

The Radó triangulation of a compact Eval surface has connected fixed-vertex stars.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_polygonalRealization_certificates (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : (compactEvalSurfaceFiniteCyclicPresentation S).IsSurfaceValid ∧ TriangleFamily.IsDualConnected (compactEvalSurfaceGeometricTriangulation S).faces ∧ TriangleFamily.IsStrongVertexStarConnected (compactEvalSurfaceGeometricTriangulation S).faces

The Eval-surface triangulation simultaneously carries cyclic validity, dual connectivity, and the fixed-star connectivity used by the faithful geometric quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_polygonalRealization_homeomorphic (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty ((compactEvalSurfaceFiniteCyclicPresentation S).PolygonalRealization ⋯ ≃ₜ ↑(compactEvalSurfaceGeometricTriangulation S).realization)

The polygonal quotient enumerated from the Radó triangulation is homeomorphic to its honest barycentric geometric realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.compact_eval_surface_polygonalRealization_homeomorphic_surface (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty ((compactEvalSurfaceFiniteCyclicPresentation S).PolygonalRealization ⋯ ≃ₜ S)

Surface-level form of the geometric bridge: the valid polygonal quotient obtained from the named Radó triangulation is homeomorphic to the original compact Eval surface.