PL certificates for the elementary Schoenflies moves

The topological homeomorphisms used by the Chapter 3 ear shelling were constructed earlier by barycentric repositioning. This file records the missing PL certificates used in Chapter 5.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.extendHomeomorphByIdentity_image {P : Set Plane} (hP : IsClosed P) (e : ↑P ≃ₜ ↑P) (hfrontier : ∀ (x : Plane) (hx : x ∈ frontier P), ↑(e ⟨x, ⋯⟩) = x) : ⇑(extendHomeomorphByIdentity hP e hfrontier) '' P = P

Extending a self-homeomorphism of a closed patch by the identity preserves that patch setwise.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorphFinitePL (e : Plane ≃ᵃ[ℝ] Plane) (K : PlaneComplex) (hpure : K.IsPure2) : FinitePLHomeomorphOn (affineEquivHomeomorph e) K.support

An affine equivalence is finite PL on the support of any explicit pure complex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.affineEquivHomeomorphFinitePL e K hpure = { complex := K, support_eq := ⋯, pure := hpure, affineOn := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryFaces (M : TriangleMesh) : Finset (Finset M.Vertex)

All nonempty faces of the incidence-one edges of a triangle mesh.

Equations

• M.boundaryFaces = M.allBoundaryEdges.biUnion fun (e : Finset M.Vertex) => {x ∈ e.powerset | x.Nonempty}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_boundaryFaces_iff (M : TriangleMesh) {s : Finset M.Vertex} : s ∈ M.boundaryFaces ↔ s.Nonempty ∧ ∃ e ∈ M.allBoundaryEdges, s ⊆ e

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryComplex (M : TriangleMesh) : PlaneComplex

The incidence-one edges and their faces form a finite one-dimensional plane complex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryComplex_support (M : TriangleMesh) : M.boundaryComplex.support = M.boundaryCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.boundaryComplex_simplex_mem_toPlaneComplex (M : TriangleMesh) {s : Finset M.Vertex} (hs : s ∈ M.boundaryComplex.simplexes) : s ∈ M.toPlaneComplex.simplexes

Every boundary-complex face is a face of the full mesh complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.ambientRepositionHomeomorph_eq_repositionMap_on_support (M : TriangleMesh) (position' : M.Vertex → Plane) (hinj : Function.Injective position') (haffTriangle : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (hinterTriangle : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (hsupport : (M.reposition position' hinj haffTriangle hinterTriangle).toPlaneComplex.support = M.toPlaneComplex.support) (hfrontier : ∀ (x : Plane) (hx : x ∈ frontier M.toPlaneComplex.support), ↑(((M.repositionHomeomorph position' hinj haffTriangle hinterTriangle).trans (Homeomorph.setCongr hsupport)) ⟨x, ⋯⟩) = x) : Set.EqOn (⇑(M.ambientRepositionHomeomorph position' hinj haffTriangle hinterTriangle hsupport hfrontier)) (M.toPlaneComplex.repositionMap position' hinj ⋯ ⋯) M.toPlaneComplex.support

On its closed patch, an ambient barycentric repositioning agrees with the facewise-affine PlaneComplex.repositionMap.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.ambientRepositionHomeomorph_affineOn (M : TriangleMesh) (position' : M.Vertex → Plane) (hinj : Function.Injective position') (haffTriangle : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (hinterTriangle : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (hsupport : (M.reposition position' hinj haffTriangle hinterTriangle).toPlaneComplex.support = M.toPlaneComplex.support) (hfrontier : ∀ (x : Plane) (hx : x ∈ frontier M.toPlaneComplex.support), ↑(((M.repositionHomeomorph position' hinj haffTriangle hinterTriangle).trans (Homeomorph.setCongr hsupport)) ⟨x, ⋯⟩) = x) {s : Finset M.Vertex} (hs : s ∈ M.toPlaneComplex.simplexes) : IsAffineOn (⇑(M.ambientRepositionHomeomorph position' hinj haffTriangle hinterTriangle hsupport hfrontier)) (M.toPlaneComplex.cellCarrier s)

An ambient barycentric repositioning is affine on every face of its source mesh.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.ambientRepositionHomeomorphFinitePL (M : TriangleMesh) (position' : M.Vertex → Plane) (hinj : Function.Injective position') (haffTriangle : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (hinterTriangle : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (hsupport : (M.reposition position' hinj haffTriangle hinterTriangle).toPlaneComplex.support = M.toPlaneComplex.support) (hfrontier : ∀ (x : Plane) (hx : x ∈ frontier M.toPlaneComplex.support), ↑(((M.repositionHomeomorph position' hinj haffTriangle hinterTriangle).trans (Homeomorph.setCongr hsupport)) ⟨x, ⋯⟩) = x) : FinitePLHomeomorphOn (M.ambientRepositionHomeomorph position' hinj haffTriangle hinterTriangle hsupport hfrontier) M.toPlaneComplex.support

An ambient barycentric repositioning, together with its original mesh, is a finite PL homeomorphism on the closed patch.

Equations

• M.ambientRepositionHomeomorphFinitePL position' hinj haffTriangle hinterTriangle hsupport hfrontier = { complex := M.toPlaneComplex, support_eq := ⋯, pure := ⋯, affineOn := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanAmbientHomeomorphFinitePL (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : FinitePLHomeomorphOn (diamondFanAmbientHomeomorph a b ha0 ha1 hb0 hb1) diamondPatch

The elementary diamond fan move is a finite PL homeomorphism on the diamond.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diamondFanAmbientHomeomorph_image (a b : ℝ) (ha0 : -2 < a) (ha1 : a < 2) (hb0 : -2 < b) (hb1 : b < 2) : ⇑(diamondFanAmbientHomeomorph a b ha0 ha1 hb0 hb1) '' diamondPatch = diamondPatch

The outer kite coordinate change

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteLeftAffine (δ : ℝ) : Plane →ᵃ[ℝ] Plane

The affine formula for thinKiteMap on the left half-plane.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteRightAffine (δ : ℝ) : Plane →ᵃ[ℝ] Plane

The affine formula for thinKiteMap on the right half-plane.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap_eq_leftAffine (δ : ℝ) {p : Plane} (hp : p.ofLp 0 ≤ 0) : thinKiteMap δ p = (thinKiteLeftAffine δ) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteMap_eq_rightAffine (δ : ℝ) {p : Plane} (hp : 0 ≤ p.ofLp 0) : thinKiteMap δ p = (thinKiteRightAffine δ) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.nonpos_zero_of_mem_axisKite_left {lo hi : ℝ} {p : Plane} (hp : p ∈ (convexHull ℝ) (axisKitePosition lo hi '' ↑{0, 2, 3})) : p.ofLp 0 ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.nonneg_zero_of_mem_axisKite_right {lo hi : ℝ} {p : Plane} (hp : p ∈ (convexHull ℝ) (axisKitePosition lo hi '' ↑{1, 2, 3})) : 0 ≤ p.ofLp 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteGlobalHomeomorphFinitePL (δ : ℝ) (hδ : 0 < δ) : FinitePLHomeomorphOn (thinKiteGlobalHomeomorph δ hδ) diamondPatch

The explicit global change from the fixed diamond to a thin kite is finite PL on the diamond's two-triangle mesh.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteGlobalHomeomorph_image (δ : ℝ) (hδ : 0 < δ) : ⇑(thinKiteGlobalHomeomorph δ hδ) '' diamondPatch = thinKitePatch δ

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorphFinitePL (δ : ℝ) (hδ : 0 < δ) : FinitePLHomeomorphOn (thinKiteAmbientHomeomorph δ hδ) (thinKitePatch δ)

The normalized thin-kite shelling move is finite PL on its kite patch.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.thinKiteAmbientHomeomorph_image (δ : ℝ) (hδ : 0 < δ) : ⇑(thinKiteAmbientHomeomorph δ hδ) '' thinKitePatch δ = thinKitePatch δ

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorphFinitePL (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) : FinitePLHomeomorphOn (transportedThinKiteHomeomorph e δ hδ) (transportedThinKitePatch e δ)

Affine transport preserves the finite-PL certificate for the local thin-kite move.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorph_image (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) : ⇑(transportedThinKiteHomeomorph e δ hδ) '' transportedThinKitePatch e δ = transportedThinKitePatch e δ

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorphFinitePLOn (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) (K : PlaneComplex) (hKpure : K.IsPure2) : FinitePLHomeomorphOn (transportedThinKiteHomeomorph e δ hδ) K.support

A transported local move is finite PL on any finite pure source polyhedron.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.transportedThinKiteHomeomorphSymmFinitePLOn (e : Plane ≃ᵃ[ℝ] Plane) (δ : ℝ) (hδ : 0 < δ) (K : PlaneComplex) (hKpure : K.IsPure2) : FinitePLHomeomorphOn (transportedThinKiteHomeomorph e δ hδ).symm K.support

The inverse transported local move is likewise finite PL on any finite pure polyhedron.

Equations

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