Finite marked refinements of plane graphs

This file enlarges the edge arrangement of a finite plane graph by finitely many prescribed points. When the marks lie in the graph support, the subordinate arrangement is a subdivision of the graph and every mark is a vertex of that subdivision.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markEquiv {P : Type u_1} [Fintype P] : P ≃ Fin (Fintype.card P)

The markEquiv declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markEquiv = Fintype.equivFin P

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) : BrokenLineData Set.univ

The edge chain enlarged by an arbitrary finite family of marked points.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain_vertex_even (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (i : Fin (Fintype.card K.EdgeFace)) : (K.markedEdgeChain point).vertex ⟨2 * ↑i, ⋯⟩ = K.position (K.edgeFirst i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain_vertex_odd (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (i : Fin (Fintype.card K.EdgeFace)) : (K.markedEdgeChain point).vertex ⟨2 * ↑i + 1, ⋯⟩ = K.position (K.edgeSecond i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain_vertex_mark (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) : (K.markedEdgeChain point).vertex ⟨2 * Fintype.card K.EdgeFace + ↑(markEquiv p), ⋯⟩ = point p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain_vertex_original (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (i : Fin (Fintype.card K.Vertex)) : (K.markedEdgeChain point).vertex ⟨2 * Fintype.card K.EdgeFace + Fintype.card P + ↑i, ⋯⟩ = K.position (K.vertexAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChainIndex (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (i : Fin (Fintype.card K.EdgeFace)) : Fin (K.markedEdgeChain point).n

The markedEdgeChainIndex declaration.

Equations

• K.markedEdgeChainIndex point i = ⟨2 * ↑i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChain_segment (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (i : Fin (Fintype.card K.EdgeFace)) : segment ℝ ((K.markedEdgeChain point).vertex (K.markedEdgeChainIndex point i).castSucc) ((K.markedEdgeChain point).vertex (K.markedEdgeChainIndex point i).succ) = K.cellCarrier ↑(K.edgeAt i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeArrangement (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) : PlaneComplex

The markedEdgeArrangement declaration.

Equations

• K.markedEdgeArrangement point = (K.markedEdgeChain point).arrangementMesh.toPlaneComplex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeSubdivision (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) : PlaneComplex

The markedEdgeSubdivision declaration.

Equations

• K.markedEdgeSubdivision point = (K.markedEdgeArrangement point).subordinateTo K

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeSubdivision_support_eq (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : (K.markedEdgeSubdivision point).support = K.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_markedEdgeSubdivision_face_at (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) {s : Finset K.Vertex} (hs : s ∈ K.simplexes) {x : Plane} (hxs : x ∈ K.cellCarrier s) : ∃ u ∈ (K.markedEdgeSubdivision point).simplexes, x ∈ (K.markedEdgeSubdivision point).cellCarrier u ∧ (K.markedEdgeSubdivision point).cellCarrier u ⊆ K.cellCarrier s

Every point of an original graph face is covered by a marked-subdivision face lying in that same original face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeSubdivision_restrictToSet_support_eq (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) (A : Set Plane) (hA : ∀ x ∈ A, ∃ s ∈ K.simplexes, x ∈ K.cellCarrier s ∧ K.cellCarrier s ⊆ A) : ((K.markedEdgeSubdivision point).restrictToSet A).support = A

Restricting a marked edge subdivision to a union of original graph faces preserves exactly that union.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeSubdivision_subdivides (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (hgraph : ∀ s ∈ K.simplexes, s.card ≤ 2) : (K.markedEdgeSubdivision point).Subdivides K

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeChainMarkIndex (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) : Fin ((K.markedEdgeChain point).n + 1)

The markedEdgeChainMarkIndex declaration.

Equations

• K.markedEdgeChainMarkIndex point p = ⟨2 * Fintype.card K.EdgeFace + ↑(LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markEquiv p), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeArrangement_monochromatic_vertical (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) : (K.markedEdgeChain point).arrangementMesh.IsMonochromatic (BrokenLineData.verticalLine (point p))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedEdgeArrangement_monochromatic_horizontal (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) : (K.markedEdgeChain point).arrangementMesh.IsMonochromatic (BrokenLineData.horizontalLine (point p))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedFace_parameter_side (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) (i : Fin (Fintype.card K.EdgeFace)) (r : ℝ) (hpoint : point p = (AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) r) {u : Finset (K.markedEdgeChain point).arrangementMesh.Vertex} (hu : u ∈ (K.markedEdgeChain point).arrangementMesh.toPlaneComplex.simplexes) : (∀ v ∈ u, (K.edgeParameter i) ((K.markedEdgeChain point).arrangementMesh.position v) ≤ r) ∨ ∀ v ∈ u, r ≤ (K.edgeParameter i) ((K.markedEdgeChain point).arrangementMesh.position v)

Every arrangement face lies on one side of a marked affine parameter on an original edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.markedFaceCarrier_parameter_side (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) (i : Fin (Fintype.card K.EdgeFace)) (r : ℝ) (hpoint : point p = (AffineMap.lineMap (K.position (K.edgeFirst i)) (K.position (K.edgeSecond i))) r) {u : Finset (K.markedEdgeChain point).arrangementMesh.Vertex} (hu : u ∈ (K.markedEdgeChain point).arrangementMesh.toPlaneComplex.simplexes) : (∀ x ∈ (K.markedEdgeChain point).arrangementMesh.toPlaneComplex.cellCarrier u, (K.edgeParameter i) x ≤ r) ∨ ∀ x ∈ (K.markedEdgeChain point).arrangementMesh.toPlaneComplex.cellCarrier u, r ≤ (K.edgeParameter i) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_face_containing_axis_segment_of_no_vertex (L : PlaneComplex) {n a b : ℝ} (hn : 0 ≤ n) (hab : a ≤ b) (ha : 0 ≤ a) (hb : b ≤ n) (hsupport : L.support = segment ℝ (planePoint 0 0) (planePoint n 0)) (hcard : ∀ s ∈ L.simplexes, s.card ≤ 2) (havoid : ∀ (v : L.Vertex), (L.position v).ofLp 0 ≤ a ∨ b ≤ (L.position v).ofLp 0) : ∃ s ∈ L.simplexes, segment ℝ (planePoint a 0) (planePoint b 0) ⊆ L.cellCarrier s

In a finite complex covering an axis segment, a subsegment with no complex vertex in its relative interior is contained in one face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.card_le_two_of_cellCarrier_subset_face {L K : PlaneComplex} {u : Finset L.Vertex} (hu : u ∈ L.simplexes) {t : Finset K.Vertex} (ht : t ∈ K.simplexes) (htcard : t.card ≤ 2) (hut : L.cellCarrier u ⊆ K.cellCarrier t) : u.card ≤ 2

A genuine simplex contained in a graph face has at most two vertices.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PlaneComplex.exists_markedEdgeSubdivision_vertex (K : PlaneComplex) {P : Type u_1} [Fintype P] (point : P → Plane) (p : P) (hp : point p ∈ K.support) : ∃ (w : (K.markedEdgeSubdivision point).Vertex), {w} ∈ (K.markedEdgeSubdivision point).simplexes ∧ (K.markedEdgeSubdivision point).position w = point p

Every prescribed mark in the graph support becomes a zero-face of the marked subdivision.