A conforming plane model of an intrinsic replacement graph #
The first intrinsic graph replacement need not be metrically close to the original embedding; its role here is to polygonalize the abstract finite graph once. A common segment arrangement turns all replacement edges into one plane graph complex. The original embedding can then be transferred to that plane complex and the ordinary plane one-skeleton approximation theorem can be applied at an arbitrary tolerance.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_cellCarrier_eq_segment
(L : PlaneComplex)
{s : Finset L.Vertex}
(hs : s ∈ L.simplexes)
(hcard : s.card ≤ 2)
:
A nonempty face of cardinality at most two is the segment between two (possibly equal) vertex positions.
@[reducible, inline]
abbrev
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.ReplacementSegmentFace
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
A one- or two-vertex face from one finite complete-edge target complex. These faces form a finite segment cover of the corresponding complete replacement edge.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementSegmentLeft
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(q : ReplacementSegmentFace)
:
First endpoint of a selected replacement segment.
Equations
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementSegmentRight
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(q : ReplacementSegmentFace)
:
Second endpoint of a selected replacement segment.
Equations
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementSegment_eq_cellCarrier
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(q : ReplacementSegmentFace)
:
segment ℝ (replacementSegmentLeft q) (replacementSegmentRight q) = (K.replacementArc hcont hinj D C q.fst).completeTarget.cellCarrier ↑q.snd
def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphCarrier
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
Union of all selected segment faces over all complete replacement edges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphArrangement
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
The common arrangement used to reconcile every edge's independent finite target complex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphBaseComplex
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
Restrict the common arrangement to the actual replacement segments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphComplex
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
The conforming finite plane graph complex of the simultaneous intrinsic replacement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphBaseComplex_support
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphComplex_support
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphCarrier_eq_image
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphComplex_support_eq_image
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_replacementGraphComplex_face_of_mem_completeCarrier
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(e : K.Edge)
{x : Plane}
(hx : x ∈ (K.replacementArc hcont hinj D C e).completeCarrier)
:
∃ s ∈ replacementGraphComplex.simplexes,
x ∈ replacementGraphComplex.cellCarrier s ∧ replacementGraphComplex.cellCarrier s ⊆ (K.replacementArc hcont hinj D C e).completeCarrier
Every point of one complete replacement edge has a face of the conforming global graph complex which remains inside that edge.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePolygonalCircle_locallyCoveredBy_replacementGraphComplex
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(t : K.Face)
(x : Plane)
:
x ∈ (facePolygonalCircle t).carrier →
∃ s ∈ replacementGraphComplex.simplexes,
x ∈ replacementGraphComplex.cellCarrier s ∧ replacementGraphComplex.cellCarrier s ⊆ (facePolygonalCircle t).carrier
Each intrinsic face polygon is locally covered by faces of the one global conforming graph complex.
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphComplex_support_eq_range
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
replacementGraphComplex.support = Set.range fun (x : ↑K.oneSkeleton) => K.graphReplacementMap hcont hinj D C ↑x
noncomputable def
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphHomeomorph
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
:
The intrinsic one-skeleton is homeomorphic to the support of its conforming polygonal plane graph model.
Equations
Instances For
@[simp]
theorem
LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.replacementGraphHomeomorph_coe
{K : IntrinsicTwoComplex}
{h : K.realization → Plane}
{hcont : Continuous h}
{hinj : Function.Injective h}
{D : K.VertexDiskControl h}
{C : K.CentralTubeControl hcont hinj D}
(x : ↑K.oneSkeleton)
: