Standard plane models for locally finite faces

A maximal face of a LocallyFiniteTriangleComplex is already parametrized by a standard simplex on its three literal global vertices. This file reindexes those coordinates by the chosen cyclic Fin 3 ordering and identifies the result with the standard closed plane triangle. The cyclic sides are carried exactly to the corresponding standard polygon sides.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceRegion : Set Plane

The closed standard triangle used as the source model for every locally finite face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceRegion = LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.support

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.StandardFaceBoundary : Type

The frontier of the standard source triangle, as a subtype.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceBoundary_mem_region (p : StandardFaceBoundary) : ↑p ∈ standardFaceRegion

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.ClosedFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Set (↥(K.faceVertices f) → ℝ)

One closed maximal face in its native simplex coordinates.

Equations

• K.ClosedFace f = stdSimplex ℝ ↥(K.faceVertices f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexToStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (x : ↑(K.ClosedFace f)) : ↑(stdSimplex ℝ (Fin 3))

Reindex native face coordinates by the chosen cyclic Fin 3 ordering.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexFromStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (z : ↑(stdSimplex ℝ (Fin 3))) : ↑(K.ClosedFace f)

Undo the cyclic coordinate reindexing.

Equations

• K.faceReindexFromStandard f z = ⟨fun (v : ↥(K.faceVertices f)) => z ((K.faceVertexEquiv f).symm v), ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexFromStandard_toStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (x : ↑(K.ClosedFace f)) : K.faceReindexFromStandard f (K.faceReindexToStandard f x) = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexToStandard_fromStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (z : ↑(stdSimplex ℝ (Fin 3))) : K.faceReindexToStandard f (K.faceReindexFromStandard f z) = z

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_faceReindexToStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Continuous (K.faceReindexToStandard f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_faceReindexFromStandard {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Continuous (K.faceReindexFromStandard f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexHomeomorph {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : ↑(K.ClosedFace f) ≃ₜ ↑(stdSimplex ℝ (Fin 3))

Native face coordinates are canonically homeomorphic to stdSimplex ℝ (Fin 3).

Equations

• K.faceReindexHomeomorph f = { toFun := K.faceReindexToStandard f, invFun := K.faceReindexFromStandard f, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardSimplexToRealization (z : ↑(stdSimplex ℝ (Fin 3))) : standardTrianglePlaneComplex.toIntrinsic.realization

Insert a standard simplex point into the one-face intrinsic realization used by the standard plane triangle complex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardSimplexToRealization z = ⟨↑z, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardRealizationToSimplex (z : standardTrianglePlaneComplex.toIntrinsic.realization) : ↑(stdSimplex ℝ (Fin 3))

Forget the vacuous one-face support witness in the standard intrinsic realization.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardRealizationToSimplex z = ⟨↑z, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardRealizationToSimplex_toRealization (z : ↑(stdSimplex ℝ (Fin 3))) : standardRealizationToSimplex (standardSimplexToRealization z) = z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardSimplexToRealization_toSimplex (z : standardTrianglePlaneComplex.toIntrinsic.realization) : standardSimplexToRealization (standardRealizationToSimplex z) = z

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardSimplexRealizationHomeomorph : ↑(stdSimplex ℝ (Fin 3)) ≃ₜ standardTrianglePlaneComplex.toIntrinsic.realization

The standard simplex and the canonical intrinsic realization of the standard triangle are the same topological simplex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdge_subset_faceVertices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : ↑(K.faceEdge f i) ⊆ K.faceVertices f

A cyclic face edge is contained in the face which names it.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeFirst_faceEdge_mem_face {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.edgeFirst (K.faceEdge f i) ∈ K.faceVertices f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSecond_faceEdge_mem_face {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.edgeSecond (K.faceEdge f i) ∈ K.faceVertices f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneHomeomorph {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : ↑(K.ClosedFace f) ≃ₜ ↑standardTrianglePlaneComplex.support

The standard plane realization of one locally finite closed face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexEmbedding {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) : Fin 3 ↪ K.Vertex

The chosen ordering of a locally finite face, viewed in the global vertex type.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeFirstIndex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : Fin 3

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

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSecondIndex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : Fin 3

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

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexEmbedding_faceEdgeFirstIndex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : (K.faceVertexEmbedding f) (K.faceEdgeFirstIndex f i) = K.edgeFirst (K.faceEdge f i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceVertexEmbedding_faceEdgeSecondIndex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : (K.faceVertexEmbedding f) (K.faceEdgeSecondIndex f i) = K.edgeSecond (K.faceEdge f i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceStandardEdge_eq_endpointIndices {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : IntrinsicTwoComplex.faceStandardEdge i = {K.faceEdgeFirstIndex f i, K.faceEdgeSecondIndex f i}

The two standard indices of cyclic side i, ordered by the global abstract edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (r : ℝ) : Plane

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

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeParameterAffine {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : Plane →ᵃ[ℝ] ℝ

The affine barycentric coordinate along the globally oriented standard side.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeParameterAffine_sourcePoint {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (r : ℝ) : (K.faceEdgeParameterAffine f i) (K.faceEdgeSourcePoint f i r) = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_mem_standardEdge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : K.faceEdgeSourcePoint f i r ∈ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_image_Icc {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : K.faceEdgeSourcePoint f i '' Set.Icc 0 1 = standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceSide {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : Set ↑(K.ClosedFace f)

Native face-simplex points supported on cyclic edge i.

Equations

• K.faceSide f i = {x : ↑(K.ClosedFace f) | ∀ (v : ↥(K.faceVertices f)), ↑v ∉ ↑(K.faceEdge f i) → x v = 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportedOnEdge_endpoint_sum {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (x : ↑(K.ClosedFace f)) (hx : ∀ (v : ↥(K.faceVertices f)), ↑v ∉ ↑e → x v = 0) : x ⟨K.edgeFirst e, ⋯⟩ + x ⟨K.edgeSecond e, ⋯⟩ = 1

The two endpoint coordinates of a face point supported on an edge add to one.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceSide_endpoint_sum {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (x : ↑(K.ClosedFace f)) (hx : x ∈ K.faceSide f i) : x ⟨K.edgeFirst (K.faceEdge f i), ⋯⟩ + x ⟨K.edgeSecond (K.faceEdge f i), ⋯⟩ = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.supportedOnEdgeToSimplex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (x : ↑(K.ClosedFace f)) (_hx : ∀ (v : ↥(K.faceVertices f)), ↑v ∉ ↑e → x v = 0) : ↑(stdSimplex ℝ ↥↑e)

Restrict a face-simplex point supported on an arbitrary incident edge.

Equations

• K.supportedOnEdgeToSimplex f e hef x _hx = K.edgeSimplexPath e ⟨x ⟨K.edgeSecond e, ⋯⟩, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceSideToEdgeSimplex {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (x : ↑(K.ClosedFace f)) (hx : x ∈ K.faceSide f i) : ↑(stdSimplex ℝ ↥↑(K.faceEdge f i))

Restrict a face-simplex point supported on side i to the corresponding edge simplex.

Equations

• K.faceSideToEdgeSimplex f i x hx = K.supportedOnEdgeToSimplex f (K.faceEdge f i) ⋯ x hx

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_mem_edgeCarrier_of_supportedOnEdge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (x : ↑(K.ClosedFace f)) (hx : ∀ (v : ↥(K.faceVertices f)), ↑v ∉ ↑e → x v = 0) : K.faceMap f x ∈ K.edgeCarrier e

A face point supported on an incident edge maps into that edge carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_mem_edgeCarrier_of_mem_faceSide {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (x : ↑(K.ClosedFace f)) (hx : x ∈ K.faceSide f i) : K.faceMap f x ∈ K.edgeCarrier (K.faceEdge f i)

A point of a native face side maps into the corresponding ambient edge carrier.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexInFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (z : ↑(stdSimplex ℝ ↥↑e)) : ↑(K.ClosedFace f)

Include edge-local simplex coordinates in any incident maximal face.

Equations

• K.edgeSimplexInFace f e hef z = stdSimplex.map (fun (v : ↥↑e) => ⟨↑v, ⋯⟩) z

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMap_edgeSimplexInFace {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (z : ↑(stdSimplex ℝ ↥↑e)) : K.faceMap f (K.edgeSimplexInFace f e hef z) = K.edgeMap e z

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeSimplexInFace_supported {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) (z : ↑(stdSimplex ℝ ↥↑e)) (v : ↥(K.faceVertices f)) (hv : ↑v ∉ ↑e) : (K.edgeSimplexInFace f e hef z) v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexToStandard_edgeSimplexPath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (r : ↑(Set.Icc 0 1)) : ↑(K.faceReindexToStandard f (K.edgeSimplexInFace f (K.faceEdge f i) ⋯ (K.edgeSimplexPath (K.faceEdge f i) r))) = (AffineMap.lineMap (Pi.single (K.faceEdgeFirstIndex f i) 1) (Pi.single (K.faceEdgeSecondIndex f i) 1)) ↑r

Reindexing the canonical edge simplex inside a face gives the same oriented affine parameter on the corresponding two standard vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneHomeomorph_edgeSimplexPath {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (r : ↑(Set.Icc 0 1)) : ↑((K.facePlaneHomeomorph f) (K.edgeSimplexInFace f (K.faceEdge f i) ⋯ (K.edgeSimplexPath (K.faceEdge f i) r))) = K.faceEdgeSourcePoint f i ↑r

The standard plane chart sends the canonical edge-simplex path to the globally oriented affine parameter on the corresponding standard side.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.edgeCarrier_subset_faceCarrier_of_subset {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (e : K.Edge) (hef : ↑e ⊆ K.faceVertices f) : K.edgeCarrier e ⊆ K.faceCarrier f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReindexToStandard_mem_faceCarrier {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) (x : ↑(K.ClosedFace f)) : standardSimplexToRealization (K.faceReindexToStandard f x) ∈ standardTrianglePlaneComplex.toIntrinsic.faceCarrier (IntrinsicTwoComplex.faceStandardEdge i) ↔ x ∈ K.faceSide f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneHomeomorph_image_edge {S : Type u_1} [TopologicalSpace S] (K : LocallyFiniteTriangleComplex S) (f : K.Face) (i : ZMod 3) : (fun (x : ↑(K.ClosedFace f)) => ↑((K.facePlaneHomeomorph f) x)) '' K.faceSide f i = standardTriangleCircle.edgeSegment i

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