Polygonal circles from cycles in finite plane complexes

A simple graph cycle in the one-skeleton of a finite plane complex is automatically a polygonal circle. The exact segment-intersection axioms follow from the complex's face-to-face law and the fact that a simple cycle has no repeated cyclic vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.cellCarrier_pair_of_adj (K : PlaneComplex) {u w : K.Vertex} : K.vertexGraph.Adj u w → K.cellCarrier {u, w} = segment ℝ (K.position u) (K.position w)

The geometric segment carried by an edge of the vertex graph.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.walkGeometricPath (K : PlaneComplex) {u w : K.Vertex} (p : K.vertexGraph.Walk u w) : Path (K.position u) (K.position w)

A graph walk traces a canonical geometric path through the corresponding straight edges.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.walkGeometricPath_nil (K : PlaneComplex) (u : K.Vertex) : K.walkGeometricPath SimpleGraph.Walk.nil = Path.refl (K.position u)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.walkGeometricPath_cons (K : PlaneComplex) {u w z : K.Vertex} (h : K.vertexGraph.Adj u w) (p : K.vertexGraph.Walk w z) : K.walkGeometricPath (SimpleGraph.Walk.cons h p) = (Path.segment (K.position u) (K.position w)).trans (K.walkGeometricPath p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.range_walkGeometricPath_subset_support (K : PlaneComplex) {u w : K.Vertex} (p : K.vertexGraph.Walk u w) (hw : {w} ∈ K.simplexes) : Set.range ⇑(K.walkGeometricPath p) ⊆ K.support

The geometric path of a walk stays in the support of the complex, provided its final vertex is an actual zero-face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.walkSegment_subset_range (K : PlaneComplex) {u w : K.Vertex} (p : K.vertexGraph.Walk u w) (i : Fin p.length) : segment ℝ (K.position (p.getVert ↑i)) (K.position (p.getVert (↑i + 1))) ⊆ Set.range ⇑(K.walkGeometricPath p)

Every straight edge of a walk occurs in the range of its geometric path.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_walkSegment_of_mem_range (K : PlaneComplex) {u w : K.Vertex} (p : K.vertexGraph.Walk u w) (hp : 0 < p.length) {x : Plane} (hx : x ∈ Set.range ⇑(K.walkGeometricPath p)) : ∃ (i : Fin p.length), x ∈ segment ℝ (K.position (p.getVert ↑i)) (K.position (p.getVert (↑i + 1)))

A nonconstant walk's geometric path is covered by its finitely many straight edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.range_walkGeometricPath_append (K : PlaneComplex) {u v w : K.Vertex} (p : K.vertexGraph.Walk u v) (q : K.vertexGraph.Walk v w) : Set.range ⇑(K.walkGeometricPath (p.append q)) = Set.range ⇑(K.walkGeometricPath p) ∪ Set.range ⇑(K.walkGeometricPath q)

Concatenating graph walks unions the ranges of their canonical geometric paths.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.range_walkGeometricPath_copy (K : PlaneComplex) {u v u' v' : K.Vertex} (p : K.vertexGraph.Walk u v) (hu : u = u') (hv : v = v') : Set.range ⇑(K.walkGeometricPath (p.copy hu hv)) = Set.range ⇑(K.walkGeometricPath p)

Changing only a walk's dependent endpoint witnesses does not change its geometric range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.range_walkGeometricPath_mapLe_restrictedTo (K : PlaneComplex) (C : Set Plane) {u v : (K.restrictedTo C).Vertex} (p : (K.restrictedTo C).vertexGraph.Walk u v) (hle : (K.restrictedTo C).vertexGraph ≤ K.vertexGraph) : Set.range ⇑(K.walkGeometricPath (SimpleGraph.Walk.mapLe hle p)) = Set.range ⇑((K.restrictedTo C).walkGeometricPath p)

Mapping a walk from a carrier restriction back to the ambient plane complex preserves its geometric range.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.copy {X : Type u_1} [TopologicalSpace X] {a b a' b' : X} (p : Path a b) (ha : a = a') (hb : b = b') : Path a' b'

Change only the endpoint witnesses of a path. Its underlying function, and hence its range and injectivity, are unchanged.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.copy p ha hb = { toFun := ⇑p, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.copy_apply {X : Type u_1} [TopologicalSpace X] {a b a' b' : X} (p : Path a b) (ha : a = a') (hb : b = b') (t : ↑unitInterval) : (copy p ha hb) t = p t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.copy_range {X : Type u_1} [TopologicalSpace X] {a b a' b' : X} (p : Path a b) (ha : a = a') (hb : b = b') : Set.range ⇑(copy p ha hb) = Set.range ⇑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.Path.range_eq_of_subset_of_injective {X : Type u_1} [TopologicalSpace X] [T2Space X] {a b : X} (arc path : Path a b) (harc : Function.Injective ⇑arc) (hsub : Set.range ⇑path ⊆ Set.range ⇑arc) : Set.range ⇑path = Set.range ⇑arc

A path contained in an embedded arc and joining the same endpoints covers that entire arc. This is the order-convexity of connected subsets of the unit interval, transported through the arc homeomorphism.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.polygonalCircleOfCycle (K : PlaneComplex) {v : K.Vertex} (p : K.vertexGraph.Walk v v) (hp : p.IsCycle) : PolygonalCircle

A simple cycle in a finite plane complex determines an honest polygonal circle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.polygonalCircleOfCycle_carrier_eq_range_walkGeometricPath (K : PlaneComplex) {v : K.Vertex} (p : K.vertexGraph.Walk v v) (hp : p.IsCycle) : (K.polygonalCircleOfCycle p hp).carrier = Set.range ⇑(K.walkGeometricPath p)

The polygonal carrier associated to a graph cycle is exactly the range of the canonical piecewise-linear path around that cycle.