Standard plane models for intrinsic faces

Every maximal face of an intrinsic complex is a closed barycentric triangle. This file gives the explicit coordinate reindexing homeomorphism to the standard plane triangle. It is the source-side bridge used to apply the already proved polygonal Schoenflies extension cellwise.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex_pure : standardTrianglePlaneComplex.IsPure2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangle_univ_mem_cells : Finset.univ ∈ standardTrianglePlaneComplex.cells

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleMeshFace : standardTrianglePlaneComplex.toTriangleMesh.Triangle

The unique maximal face of the standard triangle mesh.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangleMeshFace = ⟨Finset.univ, LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangle_univ_mem_cells⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex_support : standardTrianglePlaneComplex.support = (convexHull ℝ) (Set.range standardTriangleVertex)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTriangle_cellCarrier_univ : standardTrianglePlaneComplex.cellCarrier Finset.univ = standardTrianglePlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex_isTriangle : IsTriangle standardTrianglePlaneComplex.support

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.finEquiv_symm_three (i : ZMod 3) : (ZMod.finEquiv 3).symm i = i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexEmbedding (K : IntrinsicTwoComplex) (t : K.Face) : Fin 3 ↪ K.Vertex

The chosen ordering of one intrinsic face, viewed as an embedding into all vertices.

Equations

• K.faceVertexEmbedding t = { toFun := fun (i : Fin 3) => ↑((K.faceVertexEquiv t) i), inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge (i : ZMod 3) : Finset (Fin 3)

The two standard indices belonging to cyclic side i.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge i = {(ZMod.finEquiv 3).symm i, (ZMod.finEquiv 3).symm (i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexEmbedding_cyclic (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : (K.faceVertexEmbedding t) ((ZMod.finEquiv 3).symm i) = K.faceVertex t i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge_map (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : Finset.map (K.faceVertexEmbedding t) (faceStandardEdge i) = ↑(K.faceEdge t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge_mem_simplexes (i : ZMod 3) : faceStandardEdge i ∈ standardTrianglePlaneComplex.simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standard_cellCarrier_faceStandardEdge (i : ZMod 3) : standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i) = standardTriangleCircle.edgeSegment i

The geometric carrier of a standard cyclic edge is its polygon side.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardTriangle_oneSkeleton_support : standardTrianglePlaneComplex.oneSkeleton.support = standardTriangleCircle.carrier

The one-skeleton of the standard triangle complex is exactly its polygonal frontier.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ClosedFace (K : IntrinsicTwoComplex) (t : K.Face) : Type

One closed maximal face, as a subtype of the intrinsic realization.

Equations

• K.ClosedFace t = { x : K.realization // x ∈ K.faceCarrier ↑t }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexToStandard (K : IntrinsicTwoComplex) (t : K.Face) (x : K.ClosedFace t) : standardTrianglePlaneComplex.toIntrinsic.realization

Reindex the barycentric coordinates of an intrinsic face by its chosen Fin 3 ordering.

Equations

• K.faceReindexToStandard t x = ⟨fun (i : Fin 3) => ↑↑x ↑((K.faceVertexEquiv t) i), ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexFromStandard (K : IntrinsicTwoComplex) (t : K.Face) (z : standardTrianglePlaneComplex.toIntrinsic.realization) : K.ClosedFace t

Extend standard barycentric coordinates by zero away from the chosen intrinsic face.

Equations

• K.faceReindexFromStandard t z = ⟨⟨fun (v : K.Vertex) => if hv : v ∈ ↑t then ↑z ((K.faceVertexEquiv t).symm ⟨v, hv⟩) else 0, ⋯⟩, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexFromStandard_toStandard (K : IntrinsicTwoComplex) (t : K.Face) (x : K.ClosedFace t) : K.faceReindexFromStandard t (K.faceReindexToStandard t x) = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexToStandard_fromStandard (K : IntrinsicTwoComplex) (t : K.Face) (z : standardTrianglePlaneComplex.toIntrinsic.realization) : K.faceReindexToStandard t (K.faceReindexFromStandard t z) = z

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_faceReindexToStandard (K : IntrinsicTwoComplex) (t : K.Face) : Continuous (K.faceReindexToStandard t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexHomeomorph (K : IntrinsicTwoComplex) (t : K.Face) : K.ClosedFace t ≃ₜ standardTrianglePlaneComplex.toIntrinsic.realization

The canonical barycentric homeomorphism from one intrinsic face to the standard intrinsic triangle.

Equations

• K.faceReindexHomeomorph t = ⋯.homeoOfEquivCompactToT2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReindexToStandard_mem_faceCarrier (K : IntrinsicTwoComplex) (t : K.Face) (s : Finset (Fin 3)) (x : K.ClosedFace t) : K.faceReindexToStandard t x ∈ standardTrianglePlaneComplex.toIntrinsic.faceCarrier s ↔ ↑x ∈ K.faceCarrier (Finset.map (K.faceVertexEmbedding t) s)

Reindexing carries any selected standard subface exactly to the corresponding intrinsic vertex set.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph (K : IntrinsicTwoComplex) (t : K.Face) : K.ClosedFace t ≃ₜ ↑standardTrianglePlaneComplex.support

The standard plane realization of one intrinsic closed face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCoordRestrictionAffine (K : IntrinsicTwoComplex) (t : K.Face) : (K.Vertex → ℝ) →ᵃ[ℝ] Fin 3 → ℝ

Restrict ambient intrinsic barycentric coordinates to the ordered vertices of one face.

Equations

• K.faceCoordRestrictionAffine t = AffineMap.pi fun (j : Fin 3) => (LinearMap.proj ((K.faceVertexEmbedding t) j)).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCoordRestrictionAffine_apply (K : IntrinsicTwoComplex) (t : K.Face) (x : K.Vertex → ℝ) (j : Fin 3) : (K.faceCoordRestrictionAffine t) x j = x ((K.faceVertexEmbedding t) j)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneForwardAffine (K : IntrinsicTwoComplex) (t : K.Face) : (K.Vertex → ℝ) →ᵃ[ℝ] Plane

The forward standard-plane chart is affine in the ambient intrinsic barycentric coordinates.

Equations

• K.facePlaneForwardAffine t = LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.baryEvalAffine.comp (K.faceCoordRestrictionAffine t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_val_eq_forwardAffine (K : IntrinsicTwoComplex) (t : K.Face) (x : K.ClosedFace t) : ↑((K.facePlaneHomeomorph t) x) = (K.facePlaneForwardAffine t) ↑↑x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCoordExtensionAffine (K : IntrinsicTwoComplex) (t : K.Face) : (Fin 3 → ℝ) →ᵃ[ℝ] K.Vertex → ℝ

Affinely extend standard face coordinates by zero away from the selected intrinsic face.

Equations

• K.faceCoordExtensionAffine t = AffineMap.pi fun (v : K.Vertex) => if hv : v ∈ ↑t then (LinearMap.proj ((K.faceVertexEquiv t).symm ⟨v, hv⟩)).toAffineMap else AffineMap.const ℝ (Fin 3 → ℝ) 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCoordExtensionAffine_apply_of_mem (K : IntrinsicTwoComplex) (t : K.Face) (z : Fin 3 → ℝ) {v : K.Vertex} (hv : v ∈ ↑t) : (K.faceCoordExtensionAffine t) z v = z ((K.faceVertexEquiv t).symm ⟨v, hv⟩)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCoordExtensionAffine_apply_of_notMem (K : IntrinsicTwoComplex) (t : K.Face) (z : Fin 3 → ℝ) {v : K.Vertex} (hv : v ∉ ↑t) : (K.faceCoordExtensionAffine t) z v = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneInverseAffine (K : IntrinsicTwoComplex) (t : K.Face) : Plane →ᵃ[ℝ] K.Vertex → ℝ

The barycentric-coordinate formula for the inverse standard plane chart of one intrinsic face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneInverseAffine_standardVertex (K : IntrinsicTwoComplex) (t : K.Face) (j : Fin 3) : (K.facePlaneInverseAffine t) (standardTriangleVertex j) = Pi.single ((K.faceVertexEmbedding t) j) 1

The inverse-chart affine formula takes each standard corner to the corresponding intrinsic unit barycentric coordinate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirst_faceEdge_mem_face (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.edgeFirst (K.faceEdge t i) ∈ ↑t

The first endpoint of a cyclic face edge belongs to the containing face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecond_faceEdge_mem_face (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.edgeSecond (K.faceEdge t i) ∈ ↑t

The second endpoint of a cyclic face edge belongs to the containing face.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeFirstIndex (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : Fin 3

The standard corner corresponding to the globally chosen first endpoint of a face edge.

Equations

• K.faceEdgeFirstIndex t i = (K.faceVertexEquiv t).symm ⟨K.edgeFirst (K.faceEdge t i), ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSecondIndex (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : Fin 3

The standard corner corresponding to the globally chosen second endpoint of a face edge.

Equations

• K.faceEdgeSecondIndex t i = (K.faceVertexEquiv t).symm ⟨K.edgeSecond (K.faceEdge t i), ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexEmbedding_faceEdgeFirstIndex (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : (K.faceVertexEmbedding t) (K.faceEdgeFirstIndex t i) = K.edgeFirst (K.faceEdge t i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexEmbedding_faceEdgeSecondIndex (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : (K.faceVertexEmbedding t) (K.faceEdgeSecondIndex t i) = K.edgeSecond (K.faceEdge t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge_eq_endpointIndices (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : faceStandardEdge i = {K.faceEdgeFirstIndex t i, K.faceEdgeSecondIndex t i}

The two standard endpoint indices are exactly the cyclic standard side, with the order chosen globally by the intrinsic edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSourcePoint (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (r : ℝ) : Plane

The standard source point on a face side, oriented by the global intrinsic edge ordering.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneInverseAffine_faceEdgeSourcePoint (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (r : ℝ) : (K.facePlaneInverseAffine t) (K.faceEdgeSourcePoint t i r) = (AffineMap.lineMap (Pi.single (K.edgeFirst (K.faceEdge t i)) 1) (Pi.single (K.edgeSecond (K.faceEdge t i)) 1)) r

The inverse face chart carries the oriented standard side parameter to the corresponding intrinsic barycentric line parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneInverseAffine_faceEdgeSourcePoint_apply_second (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) (r : ℝ) : (K.facePlaneInverseAffine t) (K.faceEdgeSourcePoint t i r) (K.edgeSecond (K.faceEdge t i)) = r

On the oriented standard side, the second intrinsic barycentric coordinate is its affine parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSourcePoint_mem_standardEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : K.faceEdgeSourcePoint t i r ∈ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)

Every unit-interval source point lies on the corresponding standard side.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSourcePoint_image_Icc (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceEdgeSourcePoint t i '' Set.Icc 0 1 = standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)

The oriented unit interval covers exactly the corresponding standard side.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_symm_val (K : IntrinsicTwoComplex) (t : K.Face) (p : ↑standardTrianglePlaneComplex.support) : ↑↑((K.facePlaneHomeomorph t).symm p) = (K.facePlaneInverseAffine t) ↑p

The inverse face chart is the restriction of facePlaneInverseAffine to the closed standard triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_image_edge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : (fun (x : K.ClosedFace t) => ↑((K.facePlaneHomeomorph t) x)) '' {x : K.ClosedFace t | ↑x ∈ K.faceCarrier ↑(K.faceEdge t i)} = standardTriangleCircle.edgeSegment i

The standard plane chart sends cyclic intrinsic edge i exactly onto cyclic side i of the standard triangle.