Fine subdivisions of intrinsic two-complexes

The midpoint subdivision is quantitatively faithful: on every iteration, the image diameter of each new face is at most half that of its parent. This supplies the finite fine-subdivision and open-subcomplex extraction used in the compact form of Moise Chapter 8, Theorem 2.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePoint (K : IntrinsicTwoComplex) (t : K.Face) (v : ↥↑t) : K.realization

The barycentric realization point at a specified vertex of a specified maximal face.

Equations

• K.facePoint t v = K.vertexPoint ⟨↑v, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePoint_val (K : IntrinsicTwoComplex) (t : K.Face) (v : ↥↑t) : ↑(K.facePoint t v) = Pi.single (↑v) 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePoint_mem_faceCarrier (K : IntrinsicTwoComplex) (t : K.Face) (v : ↥↑t) : K.facePoint t v ∈ K.faceCarrier ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.sum_face_coords (K : IntrinsicTwoComplex) (t : K.Face) (x : K.realization) (hx : x ∈ K.faceCarrier ↑t) : ∑ v : ↥↑t, ↑x ↑v = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.face_affineCombination_eq (K : IntrinsicTwoComplex) (t : K.Face) (x : K.realization) (hx : x ∈ K.faceCarrier ↑t) : ((Finset.affineCombination ℝ Finset.univ fun (v : ↥↑t) => ↑(K.facePoint t v)) fun (v : ↥↑t) => ↑x ↑v) = ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.affine_mem_convexHull_facePoints (K : IntrinsicTwoComplex) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K.Face) (a : (K.Vertex → ℝ) →ᵃ[ℝ] E) (x : K.realization) (hx : x ∈ K.faceCarrier ↑t) : a ↑x ∈ (convexHull ℝ) (Set.range fun (v : ↥↑t) => a ↑(K.facePoint t v))

An affine image of a face lies in the convex hull of the images of its three vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_facePoints_dist_ge (K : IntrinsicTwoComplex) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K.Face) (a : (K.Vertex → ℝ) →ᵃ[ℝ] E) (x y : K.realization) (hx : x ∈ K.faceCarrier ↑t) (hy : y ∈ K.faceCarrier ↑t) : ∃ (v : ↥↑t) (w : ↥↑t), dist (a ↑x) (a ↑y) ≤ dist (a ↑(K.facePoint t v)) (a ↑(K.facePoint t w))

Distances in an affine image of one face are bounded by a distance between vertex images.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.affine_map_midpoint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E →ᵃ[ℝ] F) (x y : E) : a (midpoint ℝ x y) = midpoint ℝ (a x) (a y)

Affine maps preserve midpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointPosition_faceEdge (K : IntrinsicTwoComplex) (t : K.Face) (i : ZMod 3) : K.midpointPosition (Sum.inr (K.faceEdge t i)) = midpoint ℝ (Pi.single (K.faceVertex t i) 1) (Pi.single (K.faceVertex t (i + 1)) 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEval_facePoint (K : IntrinsicTwoComplex) (s : K.midpointComplex.Face) (w : ↥↑s) : ↑(K.midpointEval (K.midpointComplex.facePoint s w)) = K.midpointPosition ↑w

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.midpointEvalAffine_facePoint (K : IntrinsicTwoComplex) (s : K.midpointComplex.Face) (w : ↥↑s) : K.midpointEvalAffine ↑(K.midpointComplex.facePoint s w) = K.midpointPosition ↑w

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.MeshLE {K : IntrinsicTwoComplex} (R : K.Subdivision) (d : ℝ) : Prop

A mesh bound measured after transporting each refined face into the original realization.

Equations

• R.MeshLE d = ∀ t ∈ R.refined.faces, ∀ x ∈ R.refined.faceCarrier t, ∀ y ∈ R.refined.faceCarrier t, dist (R.homeo x) (R.homeo y) ≤ d

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.meshLE_nonneg {K : IntrinsicTwoComplex} {R : K.Subdivision} {d : ℝ} (hR : R.MeshLE d) (t : R.refined.Face) : 0 ≤ d

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.dist_midpointPosition_corner_le (K : IntrinsicTwoComplex) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K.Face) (i : ZMod 3) (a : (K.Vertex → ℝ) →ᵃ[ℝ] E) {d : ℝ} (hd : 0 ≤ d) (hvertex : ∀ (j k : ZMod 3), dist (a (Pi.single (K.faceVertex t j) 1)) (a (Pi.single (K.faceVertex t k) 1)) ≤ d) {w z : K.MidpointVertex} (hw : w ∈ K.midpointCornerFace t i) (hz : z ∈ K.midpointCornerFace t i) : dist (a (K.midpointPosition w)) (a (K.midpointPosition z)) ≤ d / 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.dist_midpointPosition_central_le (K : IntrinsicTwoComplex) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K.Face) (a : (K.Vertex → ℝ) →ᵃ[ℝ] E) {d : ℝ} (hd : 0 ≤ d) (hvertex : ∀ (j k : ZMod 3), dist (a (Pi.single (K.faceVertex t j) 1)) (a (Pi.single (K.faceVertex t k) 1)) ≤ d) {w z : K.MidpointVertex} (hw : w ∈ K.midpointCentralFace t) (hz : z ∈ K.midpointCentralFace t) : dist (a (K.midpointPosition w)) (a (K.midpointPosition z)) ≤ d / 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.meshLE_trans_midpoint {K : IntrinsicTwoComplex} (R : K.Subdivision) {d : ℝ} (hR : R.MeshLE d) : (R.trans R.refined.midpointSubdivision).MeshLE (d / 2)

One midpoint subdivision halves every existing mesh bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.refl_meshLE (K : IntrinsicTwoComplex) : (refl K).MeshLE 1

The identity subdivision has mesh at most one in barycentric sup distance.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iteratedMidpointSubdivision (K : IntrinsicTwoComplex) (n : ℕ) : K.Subdivision

The n-fold intrinsic midpoint subdivision.

Equations

• K.iteratedMidpointSubdivision 0 = LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.Subdivision.refl K
• K.iteratedMidpointSubdivision n.succ = (K.iteratedMidpointSubdivision n).trans (K.iteratedMidpointSubdivision n).refined.midpointSubdivision

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iteratedMidpointSubdivision_zero (K : IntrinsicTwoComplex) : K.iteratedMidpointSubdivision 0 = Subdivision.refl K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iteratedMidpointSubdivision_succ (K : IntrinsicTwoComplex) (n : ℕ) : K.iteratedMidpointSubdivision (n + 1) = (K.iteratedMidpointSubdivision n).trans (K.iteratedMidpointSubdivision n).refined.midpointSubdivision

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.hasSurfaceEdgeValence_iteratedMidpointSubdivision (K : IntrinsicTwoComplex) (hK : K.HasSurfaceEdgeValence) (n : ℕ) : (K.iteratedMidpointSubdivision n).refined.HasSurfaceEdgeValence

Every iterated midpoint refinement preserves the surface edge-valence bound.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.iteratedMidpointSubdivision_meshLE (K : IntrinsicTwoComplex) (n : ℕ) : (K.iteratedMidpointSubdivision n).MeshLE ((1 / 2) ^ n)

Quantitative mesh estimate for iterated midpoint subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_subdivision_mesh_lt (K : IntrinsicTwoComplex) {eps : ℝ} (heps : 0 < eps) : ∃ (R : K.Subdivision), ∀ t ∈ R.refined.faces, ∀ x ∈ R.refined.faceCarrier t, ∀ y ∈ R.refined.faceCarrier t, dist (R.homeo x) (R.homeo y) < eps

Every intrinsic finite two-complex has a faithful subdivision of arbitrarily small mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_subdivision_image_dist_lt (K : IntrinsicTwoComplex) {h : K.realization → Plane} (hcont : Continuous h) {eps : ℝ} (heps : 0 < eps) : ∃ (R : K.Subdivision), ∀ t ∈ R.refined.faces, ∀ x ∈ R.refined.faceCarrier t, ∀ y ∈ R.refined.faceCarrier t, dist (h (R.homeo x)) (h (R.homeo y)) < eps

Heine--Cantor and faithful midpoint subdivision make the image of every refined face have arbitrarily small diameter under a continuous map.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_subdivision_subordinate_openCover (K : IntrinsicTwoComplex) {I : Type u_1} (U : I → Set K.realization) (hU : ∀ (i : I), IsOpen (U i)) (hcover : Set.univ ⊆ ⋃ (i : I), U i) : ∃ (R : K.Subdivision), ∀ t ∈ R.refined.faces, ∃ (i : I), ∀ x ∈ R.refined.faceCarrier t, R.homeo x ∈ U i

A sufficiently fine intrinsic subdivision is subordinate to any open cover.

Finite subcomplexes between compact and open sets

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex (K : IntrinsicTwoComplex) (C U : Set K.realization) : Type 1

A finite subcomplex of a faithful subdivision of K, selected so that its carrier contains the prescribed compact set C and remains inside the prescribed open set U.

This is the finite-complex form of the compact part of Moise Ch. 8, Thm. 2. The full theorem in Moise treats arbitrary open subsets by a locally finite exhaustion; the Radó step only needs a finite collar around the compact part already constructed.

• subdivision : K.Subdivision

  A faithful finite refinement of the original complex.

• keptFaces : Finset (Finset self.subdivision.refined.Vertex)

  The maximal refined faces retained in the subcomplex.

• keptFaces_subset : self.keptFaces ⊆ self.subdivision.refined.faces

  Every retained face is a face of the refined complex.

• covers : C ⊆ Set.range (⇑self.subdivision.homeo ∘ self.subdivision.refined.restrictFacesInclusion fun (t : Finset self.subdivision.refined.Vertex) => t ∈ self.keptFaces)

  The selected subcomplex contains C after transport to the original realization.

• contained : Set.range (⇑self.subdivision.homeo ∘ self.subdivision.refined.restrictFacesInclusion fun (t : Finset self.subdivision.refined.Vertex) => t ∈ self.keptFaces) ⊆ U

  Its transported carrier is contained in U.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.complex {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : IntrinsicTwoComplex

The selected finite intrinsic complex.

Equations

• L.complex = L.subdivision.refined.restrictFaces fun (t : Finset L.subdivision.refined.Vertex) => t ∈ L.keptFaces

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.inclusion {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : L.complex.realization → K.realization

Its canonical map into the original realization.

Equations

• L.inclusion = ⇑L.subdivision.homeo ∘ L.subdivision.refined.restrictFacesInclusion fun (t : Finset L.subdivision.refined.Vertex) => t ∈ L.keptFaces

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.isEmbedding_inclusion {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : Topology.IsEmbedding L.inclusion

The canonical inclusion of an open subcomplex is an embedding.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.support {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : Set K.realization

The carrier of the selected subcomplex in the original realization.

Equations

• L.support = Set.range L.inclusion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.covers_support {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : C ⊆ L.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenSubcomplex.support_subset {K : IntrinsicTwoComplex} {C U : Set K.realization} (L : K.OpenSubcomplex C U) : L.support ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_openSubcomplex (K : IntrinsicTwoComplex) {C U : Set K.realization} (hC : IsCompact C) (hU : IsOpen U) (hCU : C ⊆ U) : Nonempty (K.OpenSubcomplex C U)

A compact subset of an open subset of a finite intrinsic complex is covered by a finite subcomplex of a faithful subdivision which is still contained in that open set.

Compact stages exhausting a proper open subset

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenExhaustion (K : IntrinsicTwoComplex) (U : Set K.realization) : Type 1

Finite faithful subcomplex stages exhausting an open subset of a finite intrinsic complex. Each stage contains a canonical compact distance core and lies in the interior of the next distance core. The stages are not yet a single conforming locally finite complex: reconciling their boundary subdivisions is the remaining combinatorial part of Moise Ch. 8, Thm. 2.

• stage (n : ℕ) : K.OpenSubcomplex (frontierCore U n) (interior (frontierCore U (n + 1)))

  The stage declaration.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenExhaustion.stageSupport {K : IntrinsicTwoComplex} {U : Set K.realization} (E : K.OpenExhaustion U) (n : ℕ) : Set K.realization

The carrier of one finite stage, viewed in the original realization.

Equations

• E.stageSupport n = (E.stage n).support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenExhaustion.stageSupport_subset {K : IntrinsicTwoComplex} {U : Set K.realization} (E : K.OpenExhaustion U) (hUc : Uᶜ.Nonempty) (n : ℕ) : E.stageSupport n ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.OpenExhaustion.iUnion_stageSupport {K : IntrinsicTwoComplex} {U : Set K.realization} (E : K.OpenExhaustion U) (hU : IsOpen U) (hUc : Uᶜ.Nonempty) : ⋃ (n : ℕ), E.stageSupport n = U

The finite stage carriers cover exactly the prescribed open set.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_openExhaustion (K : IntrinsicTwoComplex) {U : Set K.realization} : IsOpen U → Uᶜ.Nonempty → Nonempty (K.OpenExhaustion U)

Every proper open subset of a finite intrinsic complex has a compactly nested exhaustion by finite subcomplexes of faithful subdivisions.