Arbitrarily close intrinsic graph approximation

The first simultaneous intrinsic graph replacement polygonalizes the abstract one-skeleton but does not, by itself, give arbitrary pointwise control along a large edge. Its conforming plane model turns that replacement into an ordinary finite plane graph. Transferring the original embedding to this model and applying the plane graph approximation theorem gives the required arbitrarily close second replacement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphOriginalMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (p : Plane) : Plane

The original intrinsic embedding, transferred to the conforming plane graph model. Values off the graph support are irrelevant.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphOriginalMap_apply {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (p : ↑replacementGraphComplex.support) : replacementGraphOriginalMap ↑p = h ↑(replacementGraphHomeomorph.symm p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuousOn_replacementGraphOriginalMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} : ContinuousOn replacementGraphOriginalMap replacementGraphComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphOriginalMap_injOn {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} : Set.InjOn replacementGraphOriginalMap replacementGraphComplex.support

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (ε : ℝ) : Type

Certified output of the intrinsic one-skeleton approximation. planeMap acts on the first polygonal graph model; composing it with graphReplacementMap is the final intrinsic graph embedding.

• planeMap : Plane → Plane

  The planeMap declaration.

• isPLOnModel : IsPLOn replacementGraphComplex self.planeMap
• injOnModel : Set.InjOn self.planeMap replacementGraphComplex.support
• close (x : K.realization) : x ∈ K.oneSkeleton → dist (self.planeMap (K.graphReplacementMap hcont hinj D C x)) (h x) < ε
• facewisePL (t : K.Face) : IsPLOnSet (facePolygonalCircle t).carrier self.planeMap

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.intrinsicMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {ε : ℝ} (A : CloseGraphApproximation ε) : K.realization → Plane

The final graph map on the intrinsic realization.

Equations

• A.intrinsicMap = A.planeMap ∘ K.graphReplacementMap hcont hinj D C

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.continuousOn_intrinsicMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {ε : ℝ} (A : CloseGraphApproximation ε) : ContinuousOn A.intrinsicMap K.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.CloseGraphApproximation.injOn_intrinsicMap {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {ε : ℝ} (A : CloseGraphApproximation ε) : Set.InjOn A.intrinsicMap K.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_closeGraphApproximation {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} {ε : ℝ} (hε : 0 < ε) : Nonempty (CloseGraphApproximation ε)

Moise Ch. 6, Thm. 2 for an intrinsic finite one-skeleton: after one auxiliary polygonalization, the graph admits an arbitrarily close PL embedding, simultaneously PL on all three-edge face cycles.