Common subdivisions of finite plane triangle meshes

The finite common-refinement theorem used in Moise Chapter 5. To make a source mesh subordinate to a target mesh with the same support, cut it by every barycentric-coordinate hyperplane of every target triangle. The resulting chambers lie in target triangles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineIndependent_comp_of_injOn_convexHull {V : Type u_1} [AddCommGroup V] [Module ℝ V] (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (f : Plane →ᵃ[ℝ] V) (hf : Set.InjOn (⇑f) ((convexHull ℝ) (Set.range p))) : AffineIndependent ℝ (⇑f ∘ p)

An affine map which is injective on a nondegenerate closed triangle sends its three vertices to an affinely independent triple.

The hypothesis is deliberately local. This is the form needed when a facewise-affine embedding is known to be injective only on the simplex on which its affine formula is valid.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineMap_injective_of_injOn_convexHull (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (f : Plane →ᵃ[ℝ] Plane) (hf : Set.InjOn (⇑f) ((convexHull ℝ) (Set.range p))) : Function.Injective ⇑f

In the plane, local injectivity of an affine map on one nondegenerate triangle already forces global injectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineMap_surjective_of_injOn_convexHull (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (f : Plane →ᵃ[ℝ] Plane) (hf : Set.InjOn (⇑f) ((convexHull ℝ) (Set.range p))) : Function.Surjective ⇑f

The same local hypothesis makes a planar affine map surjective.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCoords (M : TriangleMesh) (T : M.Triangle) : Plane →ᵃ[ℝ] M.Vertex → ℝ

Barycentric coordinates in one maximal mesh triangle, extended by zero to all mesh vertices. This is the triangle-mesh-native counterpart of PlaneComplex.faceCoords; keeping the codomain definitionally equal to M.Vertex → ℝ avoids transports through M.toPlaneComplex.Vertex.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCoords_apply_of_mem (M : TriangleMesh) (T : M.Triangle) {v : M.Vertex} (hv : v ∈ ↑T) (p : Plane) : (M.triangleCoords T) p v = ((affineBasisOfTriangle (M.position ∘ M.orderedVertex T) ⋯).coord ((M.triangleEquiv T) ⟨v, hv⟩)) p

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCoords_apply_of_notMem (M : TriangleMesh) (T : M.Triangle) {v : M.Vertex} (hv : v ∉ ↑T) (p : Plane) : (M.triangleCoords T) p v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCoords_support (M : TriangleMesh) (T : M.Triangle) (p : Plane) (v : M.Vertex) : v ∉ ↑T → (M.triangleCoords T) p v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.sum_triangleCoords (M : TriangleMesh) (T : M.Triangle) (p : Plane) : ∑ v : M.Vertex, (M.triangleCoords T) p v = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.baryEval_triangleCoords (M : TriangleMesh) (T : M.Triangle) (p : Plane) : M.toPlaneComplex.baryEval ((M.triangleCoords T) p) = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleCoords_nonneg_of_mem (M : TriangleMesh) (T : M.Triangle) {p : Plane} (hp : p ∈ M.triangleCarrier ↑T) (v : M.Vertex) : 0 ≤ (M.triangleCoords T) p v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.coordinateLines (M : TriangleMesh) : List (Plane →ᵃ[ℝ] ℝ)

The barycentric-coordinate hyperplanes of all maximal triangles.

Equations

• M.coordinateLines = List.flatMap (fun (t : M.Triangle) => List.map (M.oppositeCoord t) Finset.univ.toList) Finset.univ.toList

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_mem_coordinateLines (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) : M.oppositeCoord t k ∈ M.coordinateLines

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineTo (M N : TriangleMesh) : TriangleMesh

Cut M by every coordinate hyperplane of N.

Equations

• M.refineTo N = M.refineByLines N.coordinateLines

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineTo_support (M N : TriangleMesh) : (M.refineTo N).toPlaneComplex.support = M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineTo_subdivides_left (M N : TriangleMesh) : (M.refineTo N).toPlaneComplex.Subdivides M.toPlaneComplex

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineTo_isMonochromatic (M N : TriangleMesh) (t : N.Triangle) (k : Fin 3) : (M.refineTo N).IsMonochromatic (N.oppositeCoord t k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.interior_affine_nonneg_of_surjective (f : Plane →ᵃ[ℝ] ℝ) (hf : Function.Surjective ⇑f) : interior {x : Plane | 0 ≤ f x} = {x : Plane | 0 < f x}

The interior of a nonnegative affine half-space is its strictly positive half-space.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.interior_affine_nonpos_of_surjective (f : Plane →ᵃ[ℝ] ℝ) (hf : Function.Surjective ⇑f) : interior {x : Plane | f x ≤ 0} = {x : Plane | f x < 0}

The interior of a nonpositive affine half-space is its strictly negative half-space.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_target_triangle_of_refineTo (M N : TriangleMesh) (hsupport : M.toPlaneComplex.support = N.toPlaneComplex.support) (T : (M.refineTo N).Triangle) : ∃ (U : N.Triangle), (M.refineTo N).triangleCarrier ↑T ⊆ N.triangleCarrier ↑U

Every maximal chamber of M.refineTo N lies in a maximal triangle of N, provided the two original meshes have the same support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_target_triangle_of_refineByLines_of_interior_inter_support (M N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (hlines : ∀ a ∈ N.coordinateLines, a ∈ lines) (T : (M.refineByLines lines).Triangle) (hhit : (interior ((M.refineByLines lines).triangleCarrier ↑T) ∩ N.toPlaneComplex.support).Nonempty) : ∃ (U : N.Triangle), (M.refineByLines lines).triangleCarrier ↑T ⊆ N.triangleCarrier ↑U

A chamber cut by at least all target coordinate lines and whose interior meets the target support lies in one target triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_target_triangle_of_refineTo_of_interior_inter_support (M N : TriangleMesh) (T : (M.refineTo N).Triangle) (hhit : (interior ((M.refineTo N).triangleCarrier ↑T) ∩ N.toPlaneComplex.support).Nonempty) : ∃ (U : N.Triangle), (M.refineTo N).triangleCarrier ↑T ⊆ N.triangleCarrier ↑U

A chamber whose interior meets the target support lies in one target triangle. Unlike exists_target_triangle_of_refineTo, the source and target supports need not agree.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineToSupport (M N : TriangleMesh) : TriangleMesh

Cut M by every face line of N, then retain exactly the chambers whose interiors meet the support of N. This is the unequal-support version of common refinement used in the local Radó weld.

Equations

• M.refineToSupport N = (M.refineTo N).restrictTriangles fun (t : Finset (M.refineTo N).Vertex) => (interior ((M.refineTo N).triangleCarrier t) ∩ N.toPlaneComplex.support).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineToSupport_triangle_mem (M N : TriangleMesh) {t : Finset (M.refineToSupport N).Vertex} : t ∈ (M.refineToSupport N).triangles ↔ t ∈ (M.refineTo N).triangles ∧ (interior ((M.refineTo N).triangleCarrier t) ∩ N.toPlaneComplex.support).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineToSupport_support (M N : TriangleMesh) (hsub : N.toPlaneComplex.support ⊆ M.toPlaneComplex.support) : (M.refineToSupport N).toPlaneComplex.support = N.toPlaneComplex.support

If the source mesh contains the target support, restricting their line refinement recovers the target support exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineToSupport_subdivides (M N : TriangleMesh) (hsub : N.toPlaneComplex.support ⊆ M.toPlaneComplex.support) : (M.refineToSupport N).toPlaneComplex.Subdivides N.toPlaneComplex

The support-restricted refinement is a genuine subdivision of the smaller target mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineTo_subdivides_right (M N : TriangleMesh) (hsupport : M.toPlaneComplex.support = N.toPlaneComplex.support) : (M.refineTo N).toPlaneComplex.Subdivides N.toPlaneComplex

M.refineTo N is a subdivision of N when the two meshes have the same support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_common_subdivision (M N : TriangleMesh) (hsupport : M.toPlaneComplex.support = N.toPlaneComplex.support) : ∃ (R : TriangleMesh), R.toPlaneComplex.Subdivides M.toPlaneComplex ∧ R.toPlaneComplex.Subdivides N.toPlaneComplex

Two finite plane triangle meshes with equal support have an explicit common subdivision.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toTriangleMesh (K : PlaneComplex) : TriangleMesh

Regard the two-dimensional faces of a plane complex as the maximal triangles of a mesh.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toTriangleMesh_position (K : PlaneComplex) : K.toTriangleMesh.position = K.position

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toTriangleMesh_triangles (K : PlaneComplex) : K.toTriangleMesh.triangles = K.cells

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toTriangleMesh_support (K : PlaneComplex) (hpure : K.IsPure2) : K.toTriangleMesh.toPlaneComplex.support = K.support

Passing a pure two-dimensional complex to its maximal-triangle mesh preserves support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toTriangleMesh_toPlaneComplex_subdivides (K : PlaneComplex) (hpure : K.IsPure2) : K.toTriangleMesh.toPlaneComplex.Subdivides K

The maximal-triangle mesh of a pure complex is a subdivision of the original complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_common_subdivision {K L : PlaneComplex} (hKpure : K.IsPure2) (hLpure : L.IsPure2) (hsupport : K.support = L.support) : ∃ (R : TriangleMesh), R.toPlaneComplex.Subdivides K ∧ R.toPlaneComplex.Subdivides L

Pure finite plane complexes with equal support have a common triangle-mesh subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineMap_injective_of_injOn_of_interior_nonempty (g : Plane →ᵃ[ℝ] Plane) {A : Set Plane} (hA : (interior A).Nonempty) (hinj : Set.InjOn (⇑g) A) : Function.Injective ⇑g

An affine self-map of the plane which is injective on a set with nonempty interior is injective everywhere.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplexOn (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : PlaneComplex

Map a complex through a facewise-affine map which is injective only on its support.

Unlike mapComplex, this construction does not require an irrelevant global injectivity hypothesis. The additional vertex hypothesis excludes unused vertices, whose images would not be controlled by injectivity on the support.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplexOn_cellCarrier (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : (K.mapComplexOn f hvertex hinj haffine).cellCarrier s = f '' K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplexOn_support (K : PlaneComplex) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : (K.mapComplexOn f hvertex hinj haffine).support = f '' K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsPure2.mapComplexOn (K : PlaneComplex) (hpure : K.IsPure2) (f : Plane → Plane) (hvertex : ∀ (v : K.Vertex), K.position v ∈ K.support) (hinj : Set.InjOn f K.support) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : (K.mapComplexOn f hvertex hinj haffine).IsPure2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplex (K : PlaneComplex) (f : Plane → Plane) (hinj : Function.Injective f) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : PlaneComplex

Map every face of a finite plane complex through a facewise-affine embedding.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplex_cellCarrier (K : PlaneComplex) (f : Plane → Plane) (hinj : Function.Injective f) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : (K.mapComplex f hinj haffine).cellCarrier s = f '' K.cellCarrier s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.mapComplex_support (K : PlaneComplex) (f : Plane → Plane) (hinj : Function.Injective f) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : (K.mapComplex f hinj haffine).support = f '' K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.IsPure2.mapComplex (K : PlaneComplex) (hpure : K.IsPure2) (f : Plane → Plane) (hinj : Function.Injective f) (haffine : ∀ s ∈ K.simplexes, IsAffineOn f (K.cellCarrier s)) : (K.mapComplex f hinj haffine).IsPure2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.inverse_affineOn_of_subdivides_mapComplex (K : PlaneComplex) (hpure : K.IsPure2) (h : Plane ≃ₜ Plane) (haffine : ∀ s ∈ K.simplexes, IsAffineOn (⇑h) (K.cellCarrier s)) {R : PlaneComplex} (hR : R.Subdivides (K.mapComplex ⇑h ⋯ haffine)) (s : Finset R.Vertex) : s ∈ R.simplexes → IsAffineOn (⇑h.symm) (R.cellCarrier s)

On every subdivision of the image complex, the inverse homeomorphism is affine facewise. The proof enlarges each image face to a 2-face, where its affine witness is globally invertible.