Intrinsic finite PL complexes

The complexes used during the Rado induction are not generally realized by straight triangles in one global copy of the plane. Their honest carrier is instead the canonical barycentric realization GeometricRealization. This file supplies the small intrinsic PL layer needed to state chart-transition approximation and refinement without pretending that source is planar.

A subdivision contains a homeomorphism between the two canonical realizations, together with facewise affine formulas and subordination to old faces. Thus an arbitrary homeomorphism cannot be installed as a subdivision by bookkeeping alone.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex : Type 1

A finite pure two-dimensional abstract simplicial complex. Lower-dimensional faces are implicit in the supports of the listed triangles, exactly as in GeometricRealization.

• Vertex : Type

  The Vertex declaration.

• vertexFintype : Fintype self.Vertex
• vertexDecidableEq : DecidableEq self.Vertex
• faces : Finset (Finset self.Vertex)

  The faces declaration.

• faces_card (t : Finset self.Vertex) : t ∈ self.faces → t.card = 3

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.realization (K : IntrinsicTwoComplex) : Type

The canonical barycentric realization of an intrinsic complex.

Equations

• K.realization = ↑(LeanEval.Topology.ClassificationOfSurfaces.GeometricRealization K.Vertex K.faces)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ambientFaceCarrier (K : IntrinsicTwoComplex) (t : Finset K.Vertex) : Set (K.Vertex → ℝ)

The closed barycentric carrier of a vertex set.

Equations

• K.ambientFaceCarrier t = {x : K.Vertex → ℝ | x ∈ stdSimplex ℝ K.Vertex ∧ ∀ v ∉ t, x v = 0}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier (K : IntrinsicTwoComplex) (t : Finset K.Vertex) : Set K.realization

The carrier of a listed triangle as a subset of the realization.

Equations

• K.faceCarrier t = {x : K.realization | ∀ v ∉ t, ↑x v = 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_realization_iff (K : IntrinsicTwoComplex) (x : K.Vertex → ℝ) : x ∈ GeometricRealization K.Vertex K.faces ↔ ∃ t ∈ K.faces, x ∈ K.ambientFaceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_faceCarrier_iff (K : IntrinsicTwoComplex) (t : Finset K.Vertex) (x : K.realization) : x ∈ K.faceCarrier t ↔ ∀ v ∉ t, ↑x v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier_eq_preimage (K : IntrinsicTwoComplex) (t : Finset K.Vertex) : K.faceCarrier t = Subtype.val ⁻¹' K.ambientFaceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier_closed (K : IntrinsicTwoComplex) (t : Finset K.Vertex) : IsClosed (K.faceCarrier t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.realization_eq_iUnion_faceCarrier (K : IntrinsicTwoComplex) : Set.univ = ⋃ (t : ↥K.faces), K.faceCarrier ↑t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFaces (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [DecidablePred p] : IntrinsicTwoComplex

The intrinsic subcomplex obtained by retaining a selected family of maximal faces.

Equations

• K.restrictFaces p = { Vertex := K.Vertex, vertexFintype := K.vertexFintype, vertexDecidableEq := K.vertexDecidableEq, faces := Finset.filter p K.faces, faces_card := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFaces_faces (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [DecidablePred p] : (K.restrictFaces p).faces = Finset.filter p K.faces

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFacesInclusion (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [decidablePred : DecidablePred p] : (K.restrictFaces p).realization → K.realization

The canonical inclusion of a face restriction into the old realization.

Equations

• K.restrictFacesInclusion p x = ⟨↑x, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFacesInclusion_val (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [DecidablePred p] (x : (K.restrictFaces p).realization) : ↑(K.restrictFacesInclusion p x) = ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isEmbedding_restrictFacesInclusion (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [decidablePred : DecidablePred p] : Topology.IsEmbedding (K.restrictFacesInclusion p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFacesInclusion_mem_faceCarrier_iff (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [DecidablePred p] (t : Finset K.Vertex) (x : (K.restrictFaces p).realization) : K.restrictFacesInclusion p x ∈ K.faceCarrier t ↔ x ∈ (K.restrictFaces p).faceCarrier t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.restrictFacesInclusion_range (K : IntrinsicTwoComplex) (p : Finset K.Vertex → Prop) [decidablePred : DecidablePred p] : Set.range (K.restrictFacesInclusion p) = {x : K.realization | ∃ t ∈ K.faces, p t ∧ x ∈ K.faceCarrier t}

Intrinsic vertices and edges

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edges (K : IntrinsicTwoComplex) : Finset (Finset K.Vertex)

The edges of an intrinsic two-complex.

Equations

• K.edges = K.faces.biUnion fun (t : Finset K.Vertex) => Finset.powersetCard 2 t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.HasSurfaceEdgeValence (K : IntrinsicTwoComplex) : Prop

The abstract two-complex has surface edge valence when every edge is contained in at most two maximal triangles.

Equations

• K.HasSurfaceEdgeValence = ∀ e ∈ K.edges, {t ∈ K.faces | e ⊆ t}.card ≤ 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.card_of_mem_edges (K : IntrinsicTwoComplex) {e : Finset K.Vertex} (he : e ∈ K.edges) : e.card = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_face_of_mem_edges (K : IntrinsicTwoComplex) {e : Finset K.Vertex} (he : e ∈ K.edges) : ∃ t ∈ K.faces, e ⊆ t

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Edge (K : IntrinsicTwoComplex) : Type

The finite edge type.

Equations

• K.Edge = ↥K.edges

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.oneSkeleton (K : IntrinsicTwoComplex) : Set K.realization

The intrinsic one-skeleton, as the finite union of all barycentric edge carriers.

Equations

• K.oneSkeleton = {x : K.realization | ∃ (e : K.Edge), x ∈ K.faceCarrier ↑e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_oneSkeleton_iff (K : IntrinsicTwoComplex) (x : K.realization) : x ∈ K.oneSkeleton ↔ ∃ (e : K.Edge), x ∈ K.faceCarrier ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier_edge_subset_oneSkeleton (K : IntrinsicTwoComplex) (e : K.Edge) : K.faceCarrier ↑e ⊆ K.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.oneSkeleton_eq_iUnion_faceCarrier (K : IntrinsicTwoComplex) : K.oneSkeleton = ⋃ (e : K.Edge), K.faceCarrier ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.oneSkeleton_closed (K : IntrinsicTwoComplex) : IsClosed K.oneSkeleton

Cyclic data on a maximal face

@[reducible, inline]

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

A maximal two-face of the intrinsic complex.

Equations

• K.Face = ↥K.faces

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexEquiv (K : IntrinsicTwoComplex) (t : K.Face) : Fin 3 ≃ ↥↑t

A chosen cyclic enumeration of the three vertices of a maximal face.

Equations

• K.faceVertexEquiv t = Fintype.equivOfCardEq ⋯

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

Cyclically indexed vertices of a maximal face.

Equations

• K.faceVertex t i = ↑((K.faceVertexEquiv t) ((ZMod.finEquiv 3).symm i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertex_mem (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceVertex t i ∈ ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertex_injective (K : IntrinsicTwoComplex) (t : K.Face) : Function.Injective (K.faceVertex t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertex_ne_next (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceVertex t i ≠ K.faceVertex t (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertex_ne_add_two (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceVertex t i ≠ K.faceVertex t (i + 2)

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

The intrinsic edge joining two consecutive cyclic vertices of a maximal face.

Equations

• K.faceEdge t i = ⟨{K.faceVertex t i, K.faceVertex t (i + 1)}, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_val (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : ↑(K.faceEdge t i) = {K.faceVertex t i, K.faceVertex t (i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_inter_next (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : ↑(K.faceEdge t i) ∩ ↑(K.faceEdge t (i + 1)) = {K.faceVertex t (i + 1)}

The consecutive face edges share exactly their common cyclic vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_ne_next (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.faceEdge t i ≠ K.faceEdge t (i + 1)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.UsedVertex (K : IntrinsicTwoComplex) : Type

Vertices which actually occur in a maximal face.

Equations

• K.UsedVertex = { v : K.Vertex // ∃ t ∈ K.faces, v ∈ t }

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

A cyclic face vertex with explicit evidence that it occurs in the complex.

Equations

• K.faceUsedVertex t i = ⟨K.faceVertex t i, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.usedVertexParent (K : IntrinsicTwoComplex) (v : K.UsedVertex) : Finset K.Vertex

A chosen maximal face containing a used vertex.

Equations

• K.usedVertexParent v = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.usedVertexParent_mem (K : IntrinsicTwoComplex) (v : K.UsedVertex) : K.usedVertexParent v ∈ K.faces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.usedVertex_mem_parent (K : IntrinsicTwoComplex) (v : K.UsedVertex) : ↑v ∈ K.usedVertexParent v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.vertexPoint (K : IntrinsicTwoComplex) (v : K.UsedVertex) : K.realization

The canonical barycentric point of a used vertex.

Equations

• K.vertexPoint v = ⟨Pi.single (↑v) 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_vertexPoint (K : IntrinsicTwoComplex) : Function.Injective K.vertexPoint

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.vertexPoint_mem_faceCarrier_iff (K : IntrinsicTwoComplex) (v : K.UsedVertex) (s : Finset K.Vertex) : K.vertexPoint v ∈ K.faceCarrier s ↔ ↑v ∈ s

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeParent (K : IntrinsicTwoComplex) (e : K.Edge) : Finset K.Vertex

A chosen old face containing an edge.

Equations

• K.edgeParent e = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeParent_mem (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgeParent e ∈ K.faces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edge_subset_parent (K : IntrinsicTwoComplex) (e : K.Edge) : ↑e ⊆ K.edgeParent e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirst (K : IntrinsicTwoComplex) (e : K.Edge) : K.Vertex

The chosen first endpoint of an intrinsic edge.

Equations

• K.edgeFirst e = ⋯.choose

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecond (K : IntrinsicTwoComplex) (e : K.Edge) : K.Vertex

The chosen second endpoint of an intrinsic edge.

Equations

• K.edgeSecond e = ⋯.choose

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirst_ne_edgeSecond (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgeFirst e ≠ K.edgeSecond e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edge_eq_pair (K : IntrinsicTwoComplex) (e : K.Edge) : ↑e = {K.edgeFirst e, K.edgeSecond e}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirst_mem (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgeFirst e ∈ ↑e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecond_mem (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgeSecond e ∈ ↑e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeVertexPoint (K : IntrinsicTwoComplex) (e : K.Edge) (v : K.Vertex) (hv : v ∈ ↑e) : K.realization

The canonical barycentric realization point associated to a vertex of an edge.

Equations

• K.edgeVertexPoint e v hv = ⟨Pi.single v 1, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeVertexPoint_eq_vertexPoint (K : IntrinsicTwoComplex) (e : K.Edge) (v : K.Vertex) (hv : v ∈ ↑e) : K.edgeVertexPoint e v hv = K.vertexPoint ⟨v, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirstPoint (K : IntrinsicTwoComplex) (e : K.Edge) : K.realization

Canonical first endpoint in the barycentric realization.

Equations

• K.edgeFirstPoint e = K.edgeVertexPoint e (K.edgeFirst e) ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecondPoint (K : IntrinsicTwoComplex) (e : K.Edge) : K.realization

Canonical second endpoint in the barycentric realization.

Equations

• K.edgeSecondPoint e = K.edgeVertexPoint e (K.edgeSecond e) ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirstUsed (K : IntrinsicTwoComplex) (e : K.Edge) : K.UsedVertex

The first endpoint as a used vertex.

Equations

• K.edgeFirstUsed e = ⟨K.edgeFirst e, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecondUsed (K : IntrinsicTwoComplex) (e : K.Edge) : K.UsedVertex

The second endpoint as a used vertex.

Equations

• K.edgeSecondUsed e = ⟨K.edgeSecond e, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirstUsed_ne_edgeSecondUsed (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgeFirstUsed e ≠ K.edgeSecondUsed e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.vertexPoint_edgeFirstUsed (K : IntrinsicTwoComplex) (e : K.Edge) : K.vertexPoint (K.edgeFirstUsed e) = K.edgeFirstPoint e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.vertexPoint_edgeSecondUsed (K : IntrinsicTwoComplex) (e : K.Edge) : K.vertexPoint (K.edgeSecondUsed e) = K.edgeSecondPoint e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeFirstPoint_eq_vertexPoint_of_eq (K : IntrinsicTwoComplex) (e : K.Edge) (v : K.UsedVertex) (h : K.edgeFirst e = ↑v) : K.edgeFirstPoint e = K.vertexPoint v

The canonical first endpoint depends only on its underlying used vertex, not on the chosen maximal face witnessing that the vertex is used.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgeSecondPoint_eq_vertexPoint_of_eq (K : IntrinsicTwoComplex) (e : K.Edge) (v : K.UsedVertex) (h : K.edgeSecond e = ↑v) : K.edgeSecondPoint e = K.vertexPoint v

The analogous proof-independence statement for the second endpoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdge_endpoint_order (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.edgeFirst (K.faceEdge t i) = K.faceVertex t i ∧ K.edgeSecond (K.faceEdge t i) = K.faceVertex t (i + 1) ∨ K.edgeFirst (K.faceEdge t i) = K.faceVertex t (i + 1) ∧ K.edgeSecond (K.faceEdge t i) = K.faceVertex t i

The arbitrary endpoint ordering of a cyclic face edge is one of its two cyclic orientations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath (K : IntrinsicTwoComplex) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : K.realization

The canonical interval parametrization of an intrinsic edge.

Equations

• K.edgePath e r = ⟨(AffineMap.lineMap ↑(K.edgeFirstPoint e) ↑(K.edgeSecondPoint e)) ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_edgePath (K : IntrinsicTwoComplex) (e : K.Edge) : Continuous (K.edgePath e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath_zero (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgePath e ⟨0, ⋯⟩ = K.edgeFirstPoint e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath_one (K : IntrinsicTwoComplex) (e : K.Edge) : K.edgePath e ⟨1, ⋯⟩ = K.edgeSecondPoint e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath_apply_first (K : IntrinsicTwoComplex) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑(K.edgePath e r) (K.edgeFirst e) = 1 - ↑r

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.edgePath_apply_second (K : IntrinsicTwoComplex) (e : K.Edge) (r : ↑(Set.Icc 0 1)) : ↑(K.edgePath e r) (K.edgeSecond e) = ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_edgePath (K : IntrinsicTwoComplex) (e : K.Edge) : Function.Injective (K.edgePath e)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mappedEdgePath (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : ↑(Set.Icc 0 1) → Plane

An ambient map restricted to the canonical interval of one intrinsic edge.

Equations

• K.mappedEdgePath h e = h ∘ K.edgePath e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_mappedEdgePath (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hh : Continuous h) (e : K.Edge) : Continuous (K.mappedEdgePath h e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_mappedEdgePath (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hh : Function.Injective h) (e : K.Edge) : Function.Injective (K.mappedEdgePath h e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mappedEdgePath_zero (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : K.mappedEdgePath h e ⟨0, ⋯⟩ = h (K.edgeFirstPoint e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mappedEdgePath_one (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : K.mappedEdgePath h e ⟨1, ⋯⟩ = h (K.edgeSecondPoint e)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier_inter (K : IntrinsicTwoComplex) (s t : Finset K.Vertex) : K.faceCarrier s ∩ K.faceCarrier t = K.faceCarrier (s ∩ t)

Intrinsic face carriers meet exactly in the carrier of the common vertex set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_edgePath (K : IntrinsicTwoComplex) (e : K.Edge) : Set.range (K.edgePath e) = K.faceCarrier ↑e

The canonical interval path covers exactly the barycentric carrier of its edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_edgePath_image_Ioo (K : IntrinsicTwoComplex) {e d : K.Edge} (hed : e ≠ d) : Disjoint (K.edgePath e '' {r : ↑(Set.Icc 0 1) | 0 < ↑r ∧ ↑r < 1}) (K.edgePath d '' {r : ↑(Set.Icc 0 1) | 0 < ↑r ∧ ↑r < 1})

The open barycentric carriers of distinct intrinsic edges are disjoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceCarrier_empty (K : IntrinsicTwoComplex) : K.faceCarrier ∅ = ∅

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.eq_vertexPoint_of_mem_faceCarrier_singleton (K : IntrinsicTwoComplex) (v : K.UsedVertex) (x : K.realization) (hx : x ∈ K.faceCarrier {↑v}) : x = K.vertexPoint v

A realization point supported on one used vertex is its canonical vertex point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_eq_vertexPoint_of_mem_faceCarrier_of_card_le_one (K : IntrinsicTwoComplex) (t : K.Face) {s : Finset K.Vertex} (hst : s ⊆ ↑t) (hcard : s.card ≤ 1) {x : K.realization} (hx : x ∈ K.faceCarrier s) : ∃ (v : K.UsedVertex), x = K.vertexPoint v

A nonempty barycentric carrier with at most one vertex, contained in a listed face, consists of one canonical vertex point.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_mappedEdgePath (K : IntrinsicTwoComplex) (h : K.realization → Plane) (e : K.Edge) : Set.range (K.mappedEdgePath h e) = h '' K.faceCarrier ↑e

Exact range of an intrinsic edge after applying an ambient map.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isCompact_range_mappedEdgePath (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hh : Continuous h) (e : K.Edge) : IsCompact (Set.range (K.mappedEdgePath h e))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.disjoint_range_mappedEdgePath (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hh : Function.Injective h) {e d : K.Edge} (hed : Disjoint ↑e ↑d) : Disjoint (Set.range (K.mappedEdgePath h e)) (Set.range (K.mappedEdgePath h d))

Nonincident intrinsic edges have disjoint ranges under an injective map.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnSetTo (K : IntrinsicTwoComplex) {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : K.realization → E) (A : Set K.realization) : Prop

f is affine on an intrinsic set when it is the restriction of an ambient affine map in barycentric coordinates.

Equations

• K.IsAffineOnSetTo f A = ∃ (a : (K.Vertex → ℝ) →ᵃ[ℝ] E), ∀ x ∈ A, f x = a ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnSetTo.mono (K : IntrinsicTwoComplex) {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : K.realization → E} {A B : Set K.realization} (hf : K.IsAffineOnSetTo f A) (hBA : B ⊆ A) : K.IsAffineOnSetTo f B

Restrict an intrinsic affine-on-set certificate to a smaller source set.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnSet (K : IntrinsicTwoComplex) (f : K.realization → Plane) (A : Set K.realization) : Prop

The plane-target specialization of intrinsic affinity on an arbitrary set.

Equations

• K.IsAffineOnSet f A = K.IsAffineOnSetTo f A

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnSet.continuousOn (K : IntrinsicTwoComplex) {f : K.realization → Plane} {A : Set K.realization} (hf : K.IsAffineOnSet f A) : ContinuousOn f A

Intrinsic affine-on-set maps to the plane are continuous on that set.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnFaceTo (K : IntrinsicTwoComplex) {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : K.realization → E) (t : Finset K.Vertex) : Prop

f is affine on one intrinsic face when it is the restriction of an ambient affine map in barycentric coordinates.

Equations

• K.IsAffineOnFaceTo f t = ∃ (a : (K.Vertex → ℝ) →ᵃ[ℝ] E), ∀ x ∈ K.faceCarrier t, f x = a ↑x

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnFace (K : IntrinsicTwoComplex) (f : K.realization → Plane) (t : Finset K.Vertex) : Prop

The plane-target specialization used by PL approximation.

Equations

• K.IsAffineOnFace f t = K.IsAffineOnFaceTo f t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsAffineOnFace.continuousOn (K : IntrinsicTwoComplex) {f : K.realization → Plane} {t : Finset K.Vertex} (hf : K.IsAffineOnFace f t) : ContinuousOn f (K.faceCarrier t)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision (K : IntrinsicTwoComplex) : Type 1

A faithful intrinsic subdivision. The refined realization is homeomorphic to the original; the homeomorphism is affine on each refined face and carries that face into an old face.

• refined : IntrinsicTwoComplex

  The refined declaration.

• homeo : self.refined.realization ≃ₜ K.realization

  The homeo declaration.

• affineOnFace (t : Finset self.refined.Vertex) : t ∈ self.refined.faces → ∃ (a : (self.refined.Vertex → ℝ) →ᵃ[ℝ] K.Vertex → ℝ), ∀ x ∈ self.refined.faceCarrier t, ↑(self.homeo x) = a ↑x
• subordinate (t : Finset self.refined.Vertex) : t ∈ self.refined.faces → ∃ u ∈ K.faces, ∀ x ∈ self.refined.faceCarrier t, self.homeo x ∈ K.faceCarrier u

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.refl (K : IntrinsicTwoComplex) : K.Subdivision

Every intrinsic complex is a subdivision of itself.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.refl K = { refined := K, homeo := Homeomorph.refl K.realization, affineOnFace := ⋯, subordinate := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.refl_refined (K : IntrinsicTwoComplex) : (refl K).refined = K

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.trans {K : IntrinsicTwoComplex} (R : K.Subdivision) (Q : R.refined.Subdivision) : K.Subdivision

Faithful intrinsic subdivisions compose.

Equations

• R.trans Q = { refined := Q.refined, homeo := Q.homeo.trans R.homeo, affineOnFace := ⋯, subordinate := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.trans_refined (K : IntrinsicTwoComplex) (R : K.Subdivision) (Q : R.refined.Subdivision) : (R.trans Q).refined = Q.refined

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.trans_homeo_apply (K : IntrinsicTwoComplex) (R : K.Subdivision) (Q : R.refined.Subdivision) (x : Q.refined.realization) : (R.trans Q).homeo x = R.homeo (Q.homeo x)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsPLMap (K : IntrinsicTwoComplex) (f : K.realization → Plane) : Prop

A map from an intrinsic complex to the plane is PL when it becomes affine on every face of a faithful finite subdivision.

Equations

• K.IsPLMap f = ∃ (R : K.Subdivision), ∀ t ∈ R.refined.faces, R.refined.IsAffineOnFace (f ∘ ⇑R.homeo) t

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsPLMapTo (K : IntrinsicTwoComplex) {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : K.realization → E) : Prop

The target-vector-space form of intrinsic piecewise linearity.

Equations

• K.IsPLMapTo f = ∃ (R : K.Subdivision), ∀ t ∈ R.refined.faces, R.refined.IsAffineOnFaceTo (f ∘ ⇑R.homeo) t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isPLMap_iff_isPLMapTo (K : IntrinsicTwoComplex) (f : K.realization → Plane) : K.IsPLMap f ↔ K.IsPLMapTo f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsPLMap.continuous (K : IntrinsicTwoComplex) {f : K.realization → Plane} (hf : K.IsPLMap f) : Continuous f

Intrinsic PL maps into the plane are continuous. Continuity is glued over the finite family of closed refined faces and transported back through the subdivision homeomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isPLMap_of_affine (K : IntrinsicTwoComplex) (f : K.realization → Plane) (a : (K.Vertex → ℝ) →ᵃ[ℝ] Plane) (ha : ∀ (x : K.realization), f x = a ↑x) : K.IsPLMap f

A globally affine map in barycentric coordinates is intrinsically PL.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.barycentricMap (K : IntrinsicTwoComplex) (p : K.Vertex → Plane) (x : K.realization) : Plane

The affine barycentric map determined by positions assigned to the vertices.

Equations

• K.barycentricMap p x = ∑ v : K.Vertex, ↑x v • p v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.barycentricMap_isPL (K : IntrinsicTwoComplex) (p : K.Vertex → Plane) : K.IsPLMap (K.barycentricMap p)

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.PLHomeomorph (K L : IntrinsicTwoComplex) : Type

A homeomorphism of canonical realizations that is intrinsically PL in both directions.

• toHomeomorph : K.realization ≃ₜ L.realization

  The toHomeomorph declaration.

• isPL_to : K.IsPLMapTo fun (x : K.realization) => ↑(self.toHomeomorph x)
• isPL_inv : L.IsPLMapTo fun (x : L.realization) => ↑(self.toHomeomorph.symm x)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.PLHomeomorph.refl (K : IntrinsicTwoComplex) : K.PLHomeomorph K

The identity intrinsic PL homeomorphism.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.PLHomeomorph.refl K = { toHomeomorph := Homeomorph.refl K.realization, isPL_to := ⋯, isPL_inv := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.PLHomeomorph.refl_apply (K : IntrinsicTwoComplex) (x : K.realization) : (refl K).toHomeomorph x = x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.toPLHomeomorph (K : IntrinsicTwoComplex) (R : K.Subdivision) : R.refined.PLHomeomorph K

A faithful subdivision is itself a PL homeomorphism between the refined and original realizations. For the inverse direction, use the same subdivision as the witness: after precomposition with its homeomorphism the inverse is the identity.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.toPLHomeomorph K R = { toHomeomorph := R.homeo, isPL_to := ⋯, isPL_inv := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.IsPLMap.of_subdivision (K : IntrinsicTwoComplex) (R : K.Subdivision) {f : K.realization → Plane} (hf : R.refined.IsPLMap (f ∘ ⇑R.homeo)) : K.IsPLMap f

A PL map on a refinement is PL on the original intrinsic complex.