Extending a homeomorphism of a closed planar patch

Moise's elementary free-triangle move is first constructed on a finite polygonal patch. Since the move fixes the patch frontier, it extends to an ambient homeomorphism by the identity. This file proves that pasting step independently of the particular triangulated patch.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.coe_setCongr_apply {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : s = t) (z : ↑s) : ↑((Homeomorph.setCongr h) z) = ↑z

Changing only the proof that a point belongs to an equal set does not change the point.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.repositionHomeomorph (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) : ↑M.toPlaneComplex.support ≃ₜ ↑(M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.support

Repositioning a fixed abstract triangle mesh gives a canonical homeomorphism between the old and new geometric supports, obtained by preserving barycentric coordinates.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.repositionHomeomorph_apply_realization (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (x : ↑(GeometricRealization M.toPlaneComplex.Vertex M.toPlaneComplex.cells)) : (M.repositionHomeomorph position' hposition_injective haffineIndependent htriangle_inter) ((M.toPlaneComplex.realizationHomeomorph ⋯) x) = ((M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.realizationHomeomorph ⋯) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coe_repositionHomeomorph_apply_realization (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (x : ↑(GeometricRealization M.toPlaneComplex.Vertex M.toPlaneComplex.cells)) : ↑((M.repositionHomeomorph position' hposition_injective haffineIndependent htriangle_inter) ((M.toPlaneComplex.realizationHomeomorph ⋯) x)) = (M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.baryEval ↑x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coe_repositionHomeomorph_apply (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (z : ↑M.toPlaneComplex.support) : ↑((M.repositionHomeomorph position' hposition_injective haffineIndependent htriangle_inter) z) = (M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.baryEval ↑((M.toPlaneComplex.realizationHomeomorph ⋯).symm z)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coe_repositionHomeomorph_trans_setCongr_apply (M : TriangleMesh) (position' : M.Vertex → Plane) (hposition_injective : Function.Injective position') (haffineIndependent : ∀ t ∈ M.triangles, AffineIndependent ℝ fun (v : ↥t) => position' ↑v) (htriangle_inter : ∀ s ∈ M.triangles, ∀ t ∈ M.triangles, (convexHull ℝ) (position' '' ↑s) ∩ (convexHull ℝ) (position' '' ↑t) = (convexHull ℝ) (position' '' ↑(s ∩ t))) (hsupport : (M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.support = M.toPlaneComplex.support) (z : ↑M.toPlaneComplex.support) : ↑(((M.repositionHomeomorph position' hposition_injective haffineIndependent htriangle_inter).trans (Homeomorph.setCongr hsupport)) z) = (M.reposition position' hposition_injective haffineIndependent htriangle_inter).toPlaneComplex.baryEval ↑((M.toPlaneComplex.realizationHomeomorph ⋯).symm z)

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

Extend a homeomorphism of a closed planar patch by the identity outside the patch.

Equations

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

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

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

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

A repositioning with unchanged support and fixed support frontier extends to an ambient plane homeomorphism.

Equations

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

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