Plane subdivisions as intrinsic subdivisions

The Rado induction uses intrinsic complexes, while all finite cutting and common-refinement machinery is geometric and planar. This file is the bridge between those layers. A pure plane complex is regarded as the intrinsic complex of its maximal triangles, and a geometric subdivision induces a faithful intrinsic subdivision through the barycentric realization homeomorphisms.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toIntrinsic (K : PlaneComplex) : IntrinsicTwoComplex

Forget the planar placement of a complex, retaining its maximal triangles as an intrinsic two-complex.

Equations

• K.toIntrinsic = { Vertex := K.Vertex, vertexFintype := K.vertexFintype, vertexDecidableEq := K.vertexDecidableEq, faces := K.cells, faces_card := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.toIntrinsic_faces (K : PlaneComplex) : K.toIntrinsic.faces = K.cells

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEvalAffine (K : PlaneComplex) : (K.Vertex → ℝ) →ᵃ[ℝ] Plane

Barycentric evaluation is an affine map on the ambient coordinate space.

Equations

• K.baryEvalAffine = (∑ v : K.Vertex, (LinearMap.proj v).smulRight (K.position v)).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEvalAffine_apply (K : PlaneComplex) (x : K.Vertex → ℝ) : K.baryEvalAffine x = K.baryEval x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.faceCoords (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) : Plane →ᵃ[ℝ] K.Vertex → ℝ

Barycentric coordinates in one maximal triangle, extended by zero to all vertices of the complex.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.faceCoords_apply_of_mem (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) {v : K.Vertex} (hv : v ∈ ↑T) (p : Plane) : (K.faceCoords T) p v = ((affineBasisOfTriangle (K.toTriangleMesh.position ∘ K.toTriangleMesh.orderedVertex T) ⋯).coord ((K.toTriangleMesh.triangleEquiv T) ⟨v, hv⟩)) p

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.faceCoords_apply_of_notMem (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) {v : K.Vertex} (hv : v ∉ ↑T) (p : Plane) : (K.faceCoords T) p v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.faceCoords_support (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) (p : Plane) (v : K.toTriangleMesh.Vertex) : v ∉ ↑T → (K.faceCoords T) p v = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.sum_faceCoords (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) (p : Plane) : ∑ v : K.Vertex, (K.faceCoords T) p v = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.orderedVertex_triangleEquiv (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) (v : ↥↑T) : K.toTriangleMesh.orderedVertex T ((K.toTriangleMesh.triangleEquiv T) v) = ↑v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.baryEval_faceCoords (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) (p : Plane) : K.baryEval ((K.faceCoords T) p) = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.faceCoords_position (K : PlaneComplex) (T : K.toTriangleMesh.Triangle) {v : K.Vertex} (hv : v ∈ ↑T) : (K.faceCoords T) (K.position v) = Pi.single v 1

The affine coordinates of a geometric triangle vertex are the corresponding unit barycentric coordinates.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorph_symm_mem_faceCarrier (K : PlaneComplex) (hpure : K.IsPure2) (T : K.toTriangleMesh.Triangle) (p : ↑K.support) (hp : ↑p ∈ K.cellCarrier ↑T) : (K.realizationHomeomorph hpure).symm p ∈ K.toIntrinsic.faceCarrier ↑T

The inverse barycentric realization map sends a point of a maximal geometric triangle to the corresponding intrinsic face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorph_symm_val_eq_faceCoords (K : PlaneComplex) (hpure : K.IsPure2) (T : K.toTriangleMesh.Triangle) (p : ↑K.support) (hp : ↑p ∈ K.cellCarrier ↑T) : ↑((K.realizationHomeomorph hpure).symm p) = (K.faceCoords T) ↑p

On a selected maximal triangle, the inverse realization homeomorphism is given by the explicit affine barycentric-coordinate map for that triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.realizationHomeomorph_image_faceCarrier (K : PlaneComplex) (hpure : K.IsPure2) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) : (fun (x : K.toIntrinsic.realization) => ↑((K.realizationHomeomorph hpure) x)) '' K.toIntrinsic.faceCarrier s = K.cellCarrier s

Barycentric realization carries every abstract face carrier exactly onto its geometric convex hull.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.subdivisionHomeomorph {L K : PlaneComplex} (hLpure : L.IsPure2) (hKpure : K.IsPure2) (hLK : L.Subdivides K) : L.toIntrinsic.realization ≃ₜ K.toIntrinsic.realization

The intrinsic homeomorphism underlying a geometric subdivision of pure plane complexes.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.baryEval_subdivisionHomeomorph {L K : PlaneComplex} (hLpure : L.IsPure2) (hKpure : K.IsPure2) (hLK : L.Subdivides K) (x : L.toIntrinsic.realization) : K.baryEval ↑((subdivisionHomeomorph hLpure hKpure hLK) x) = L.baryEval ↑x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.subdivisionOfPlaneSubdivision {L K : PlaneComplex} (hLpure : L.IsPure2) (hKpure : K.IsPure2) (hLK : L.Subdivides K) : K.toIntrinsic.Subdivision

A geometric subdivision of pure finite plane complexes is a faithful subdivision of their intrinsic realizations.

Equations

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