The locally finite adaptive fan triangulation

This file packages the conforming adaptive fan faces as the locally finite triangle complex used in Rado's induction. Its global vertex type contains exactly the geometric vertices which occur in a fan face. This no-junk representation is what lets compactness turn local finiteness into a finite intrinsic triangulation.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.AdaptiveFanVertex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : Type

Geometric vertices which occur in at least one adaptive fan face.

Equations

• K.AdaptiveFanVertex U hU = { p : K.realization // ∃ (f : K.AdaptiveFanFace U hU), p ∈ K.adaptiveFanFaceVertices U hU f }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanVertexEmbedding (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↥(K.adaptiveFanFaceVertices U hU f) ↪ K.AdaptiveFanVertex U hU

Include the three local vertices of one fan face in the global used-vertex type.

Equations

• K.adaptiveFanVertexEmbedding U hU f = { toFun := fun (p : ↥(K.adaptiveFanFaceVertices U hU f)) => ⟨↑p, ⋯⟩, inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceVertices (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Finset (K.AdaptiveFanVertex U hU)

The three vertices of a fan face, now regarded as global used vertices.

Equations

• K.adaptiveGlobalFanFaceVertices U hU f = Finset.map (K.adaptiveFanVertexEmbedding U hU f) (K.adaptiveFanFaceVertices U hU f).attach

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.mem_adaptiveGlobalFanFaceVertices_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (v : K.AdaptiveFanVertex U hU) : v ∈ K.adaptiveGlobalFanFaceVertices U hU f ↔ ↑v ∈ K.adaptiveFanFaceVertices U hU f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceVertexEquiv (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↥(K.adaptiveGlobalFanFaceVertices U hU f) ≃ ↥(K.adaptiveFanFaceVertices U hU f)

Relabel the local global vertices of a face by their underlying geometric points.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanFaceVertexEquiv_apply_val (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (v : ↥(K.adaptiveGlobalFanFaceVertices U hU f)) : ↑((K.adaptiveFanFaceVertexEquiv U hU f) v) = ↑↑v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanRelabelSimplex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) : ↑(stdSimplex ℝ ↥(K.adaptiveFanFaceVertices U hU f))

Relabel a simplex on global used vertices as a simplex on the face's geometric vertices.

Equations

• K.adaptiveFanRelabelSimplex U hU f x = stdSimplex.map (⇑(K.adaptiveFanFaceVertexEquiv U hU f)) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanRelabel_extended_apply (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) (x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))) (v : K.AdaptiveFanVertex U hU) : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) (K.adaptiveFanRelabelSimplex U hU f x) ↑v = extendFaceCoordinates (K.adaptiveGlobalFanFaceVertices U hU f) x v

Relabeling preserves the zero-extended coordinate at every global used vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanRelabel_extended_eq_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} {x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU g))} : extendFaceCoordinates (K.adaptiveFanFaceVertices U hU f) (K.adaptiveFanRelabelSimplex U hU f x) = extendFaceCoordinates (K.adaptiveFanFaceVertices U hU g) (K.adaptiveFanRelabelSimplex U hU g y) ↔ extendFaceCoordinates (K.adaptiveGlobalFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveGlobalFanFaceVertices U hU g) y

Equality of coordinates is invariant under relabeling a pair of adaptive fan faces.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f)) → ↑U

One adaptive fan face parametrized by its global used vertices.

Equations

• K.adaptiveGlobalFanFaceMap U hU f x = K.adaptiveFanFaceMap U hU f (K.adaptiveFanRelabelSimplex U hU f x)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_adaptiveGlobalFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Continuous (K.adaptiveGlobalFanFaceMap U hU f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_adaptiveGlobalFanFaceMap (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) : Set.range (K.adaptiveGlobalFanFaceMap U hU f) = Set.range (K.adaptiveFanFaceMap U hU f)

Relabeling a fan face by global vertices does not change its geometric range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveFanRelabeledFaceMap_eq_iff (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) {f g : K.AdaptiveFanFace U hU} {x : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU f))} {y : ↑(stdSimplex ℝ ↥(K.adaptiveGlobalFanFaceVertices U hU g))} : K.adaptiveGlobalFanFaceMap U hU f x = K.adaptiveGlobalFanFaceMap U hU g y ↔ extendFaceCoordinates (K.adaptiveGlobalFanFaceVertices U hU f) x = extendFaceCoordinates (K.adaptiveGlobalFanFaceVertices U hU g) y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGlobalFanFaceVertices_injective (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : Function.Injective (K.adaptiveGlobalFanFaceVertices U hU)

Distinct adaptive fan triangles have distinct global three-vertex sets. Equality first identifies the adaptive tile by its interior center. After erasing that center, the two base endpoint pairs agree; their common midpoint then identifies both the cyclic tile edge and the consecutive interval in its ordered boundary-vertex list.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveLocallyFiniteTriangleComplex (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : LocallyFiniteTriangleComplex ↑U

The adaptiveLocallyFiniteTriangleComplex declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveLocallyFiniteTriangleComplex_support (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) : (K.adaptiveLocallyFiniteTriangleComplex U hU).support = Set.univ

The global adaptive fan complex covers the entire open subspace.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.adaptiveGeometricTriangulation (K : IntrinsicTwoComplex) (U : Set K.realization) [K.AdaptiveSafety U] [AdaptiveSafety.IsAdmissible K U] (hU : IsOpen U) [CompactSpace ↑U] [T2Space ↑U] : GeometricTriangulation ↑U

On a compact open subspace, the adaptive locally finite complex is an honest finite geometric triangulation.

Equations

• K.adaptiveGeometricTriangulation U hU = (K.adaptiveLocallyFiniteTriangleComplex U hU).toGeometricTriangulation ⋯